I have functions (e.g. proof terms) like:
(fun (A B : Prop) (a0 a1 : A) => ?Goal).
but I’d like to print the curried version (I want to curry it):
(fun (A B : Prop) => fun (a0 a1 : A) => ?Goal).
How does one do this in Coq? It seems:
Set Printing All.
didn’t do what I wanted nor does googling “remove pretty printing in coq” lead to too many useful results.
If I can I don’t want implicit to be printed, only the uncurrying if possible. But implicit is fine if there is no other option.
- currying, In mathematics and computer science, currying is the technique of converting a function that takes multiple arguments into a sequence of functions that each takes a single argument: Currying - Wikipedia
Other seemingly related links:
you can add a notation, for instance
(* without the double space it doesn't print a space between ) and => *)
Notation "'fun' ( x : A ) => c" := (fun (x : A) => c) (at level 200, x name, right associativity, only printing).
Check fun a b : nat => a + b.
(* fun (a : nat) => fun (b : nat) => a + b *)
TBH this doesn’t seem at all useful though
For your benefit, allow me to correct you: That function is already curried.
Consider a function of type
A -> B -> C: strictly speaking, that is not a function taking two arguments, but a unary function from type
A to function type
B -> C.
More in general, Coq’s functions are all unary in the strict sense. But we typically don’t use this “strict sense”: We’ll often call that a binary function, but it’s really the curried encoding of such a function.
Currying and uncurrying still make sense in Coq: you can use curried functions
A -> B -> C or uncurried functions
(A * B) -> C; the latter are also unary functions, but their source type is the binary product
A * B.