jaewooklee93
commented
9 years ago Of course, if you do the same thing in C++, it immediately returns compile error, but Curried function is a ubiquitous feature mainly on functional programming languages like Coq.
If you give only part of necessary arguments for a function, it will not begin the computation at that time, but it becomes another function waiting for remaining arguments. Since these partially filled functions are really functions, you can pass them as arguments for higher order functions. The common example is this one.
Eval compute in map (plus 3) [5; 4; 3; 2; 1].
(* [8; 7; 6; 5; 4] *)You don't have to waste your time to define a new function for adding 3 to natural numbers.
AdamBJ
In Prop, the book defines a family of propositions "between" indexed by n m and o to be true for a particular set of n m and o if o is somewhere in the range [n m].
Definition between (n m o: nat) : Prop := andb (ble_nat n o) (ble_nat o m) = true.
Then the book goes on to define the function "teen", which returns a true proposition if the nat we give it as input is in the range [13 19].
Definition teen : nat→Prop := between 13 19.
Conceptually, I think I understand what is going on here. However, how does Coq know that the nat given as input to teen should serve as the third input to between? I would have expected Coq to produce an error when its given between 13 19 since there is no explicit third argument.