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

Using Coq
1

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:

2

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

3

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.

4

curious, how is this different from implicit and explicit args?