diff options
| author | Max Schumacher <maximilianbschumacher@gmail.com> | 2021-03-21 15:23:05 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-21 15:23:05 +0100 |
| commit | 1c5fecd845b48d595913d80dc0b29671e508e23b (patch) | |
| tree | d5aa59599fb3f621fc919dcb03b59fe3789a3a7e /coq.html.markdown | |
| parent | 44526992794e25f7945126d5be3737a3be517b2a (diff) | |
| parent | c5d94d3493c411ce6843a0f6c80b72ca16e3801e (diff) | |
Merge pull request #4140 from dbenn/patch-1
[coq/en] Update coq.html.markdown
Diffstat (limited to 'coq.html.markdown')
| -rw-r--r-- | coq.html.markdown | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/coq.html.markdown b/coq.html.markdown index fa1558e6..3a924a19 100644 --- a/coq.html.markdown +++ b/coq.html.markdown @@ -61,8 +61,8 @@ Locate "+". (* Calling a function with insufficient number of arguments does not cause an error, it produces a new function. *) -Definition make_inc x y := x + y. (* make_inc is int -> int -> int *) -Definition inc_2 := make_inc 2. (* inc_2 is int -> int *) +Definition make_inc x y := x + y. (* make_inc is nat -> nat -> nat *) +Definition inc_2 := make_inc 2. (* inc_2 is nat -> nat *) Compute inc_2 3. (* Evaluates to 5 *) |