diff options
| -rw-r--r-- | doc/tutorial/Tutorial.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 836944ab1..e09feeb8e 100644 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -208,7 +208,7 @@ Definition two : nat := S one. Actually \Coq~ allows several possible syntaxes: \begin{coq_example} -Definition three : nat := S two. +Definition three := S two : nat. \end{coq_example} Here is a way to define the doubling function, which expects an |