How to unset printing everything? (e.g. implicits, notations, etc)

Using Coq
1

I wanted to unset printing everything. For that, I started of my attempt to only unset printing notation but somehow it’s not working as I expected. e.g.

    Print my_notation_eq_fun_def.
    Unset Printing Notations.
    Print my_notation_eq_fun_def.

Prints the same as the first one:

my_notation_eq_fun_def = 
fun x1 x2 : my_nat => eq_refl
	 : forall x1 x2 : my_nat, x1 [+] x2 = x1 [+] x2

what I expect it is to remove my definition of [+] and use my add instead (my_add x y). Why is it not doing it?

Since that didn’t work I assumed trying Unset Printing Implicit. would be useless.

resources I tried:

and related SO links.

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

2

Not sure what could work in your case, missing some context from your example.
But if you want Coq to give you the most information you can try Set Printing All.

1 Like
3

that nearly did it. I also wanted to expand the definition of functions (so identifiers) but instead I get:

id' = @id
     : forall (A : Type) (_ : A), A

not @id is just pointing to id the identity function.

4

for example, how would I print the entire contents of a proof object/lambda term, expressing it only as a lambda term?

5

If the resulting term is not too big you can try `Eval delta in t.ˋ

6

Sorry this does not work (even with the right syntax Eval cbv delta in t.) because Lemmas are generally stored as opaque constants, therefore you can print them, but not unfold them in another term.