mirror of
https://github.com/adambard/learnxinyminutes-docs.git
synced 2024-12-23 09:41:36 +00:00
Merge pull request #4140 from dbenn/patch-1
[coq/en] Update coq.html.markdown
This commit is contained in:
commit
1c5fecd845
@ -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 *)
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user