iskm/learnxinyminutes-docs
1
0
Fork 0
mirror of https://github.com/adambard/learnxinyminutes-docs.git synced 2024-12-23 09:41:36 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Update coq.html.markdown

Browse Source 
Suggested correction to make_inc and inc_2 as having `nat` types rather than `int`.
This commit is contained in:
dbenn 2021-03-13 12:26:11 +10:30 committed by GitHub
parent 5d2d1cf77c
commit c5d94d3493
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
coq.html.markdown
View File

@ -61,8 +61,8 @@ Locate "+".
(* Calling a function with insufficient number of arguments does not cause (* Calling a function with insufficient number of arguments does not cause
an error, it produces a new function. *) an error, it produces a new function. *)
Definition make_inc x y := x + y. (* make_inc is int -> int -> int *) Definition make_inc x y := x + y. (* make_inc is nat -> nat -> nat *)
Definition inc_2 := make_inc 2. (* inc_2 is int -> int *) Definition inc_2 := make_inc 2. (* inc_2 is nat -> nat *)
Compute inc_2 3. (* Evaluates to 5 *) Compute inc_2 3. (* Evaluates to 5 *)