hover confusion

Stream: lean4

[Kevin Buzzard]

In the below code

inductive MyNat : Type
| zero : MyNat
| succ : MyNat → MyNat

def is_zero : MyNat → Prop
| MyNat.zero => True
| MyNat.succ _ => False


example : is_zero (MyNat.zero) = True := by
  unfold is_zero
  /-
  ⊢ (match MyNat.zero with
    | MyNat.zero => True              <---------- hover over that `MyNat.zero`
    | MyNat.succ a => False) =
    True
  -/
  sorry

just before the sorry, if I hover over the MyNat.zero in the MyNat.zero => True line (not the one in the match line), Lean reports MyNat.succ a : MyNat. Is this expected? I certainly didn't expect it.

[Damiano Testa]

I was not expecting that either, but it seems systematic: if you replace your definition of is_zero with

def is_zero : MyNat → Prop
| MyNat.zero => True
| MyNat.succ MyNat.zero => False
| MyNat.succ (MyNat.succ MyNat.zero) => False
| MyNat.succ _ => False

hovering on all the match arms displays the information of the last one.

[Damiano Testa]

In fact, if you make MyNat.zero => True be the last match, it seems that you always get info of the last arm.

[Shreyas Srinivas]

can confirm