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.