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.