# Print the curried version of a function (i.e. explicitly printing the functions as an explicit chain)

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.

references:

• 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`.