print kernel terms

Stream: lean4

[Leonard Wiechmann]

i'm trying to understand what's going on here:

theorem Fin.eq_of_val_eq {n} : ∀ {i j : Fin n}, Eq i.val j.val → Eq i j
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

sadly, #print gives me a term with match instead of recursors.
how can i print the kernel term?

[Leonard Wiechmann]

i found this option set_option trace.PrettyPrinter.delab false, but it doesn't seem to be about #print.

[Alex J. Best]

set_option pp.match false

[Leonard Wiechmann]

awesome, thanks!