Eq.ndrec vs Eq.rec

Stream: lean4

[François G. Dorais]

I just noticed that both Eq.ndrec and Eq.rec unexpand to "▸" notation:

https://github.com/leanprover/lean4/blob/474395aae486800d5ce7c7fe7e9d51a383614267/src/Init/NotationExtra.lean#L133

So it's impossible to tell them apart without disabling the "▸" notation. Is there a way to disable a single notation? Disabling all notations works but it can be hard to read very long terms that way. Is there any other way to tell Eq.ndrec from Eq.rec?

[Leonardo de Moura]

I added support for temporarily erasing keyed attributes. It includes appUnexpander, termElab, commandElab, tactic, etc. Example:

theorem ex {i j : Fin n} (h : i = j) : i.val = j.val :=
  h ▸ rfl

attribute [-appUnexpander] unexpandEqNDRec

#print ex
/-
theorem ex : ∀ {n : Nat} {i j : Fin n}, i = j → i.val = j.val :=
fun {n} {i j} h => Eq.ndrec rfl h
-/