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`

.