Getting hypothesis from match

Stream: lean4

[Markus Schmaus]

How can I get the match as a hypothesis when pattern matching? I.e. what can replace the sorry in this mwe?

structure MyStructure (α : Type) where
  s : List α

def f (x : MyStructure α) (_ : x.s = []) : Bool := true

def g (x : MyStructure α) : Bool:=
  match x.s with
  | [] =>
    have proof : x.s = [] := sorry
    f x proof
  | _ => false

For if there is the if h : x.s = [] syntax, but this doesn't work here, since α might not have a decidable =.

[Adam Topaz]

def g (x : MyStructure α) : Bool:=
  match h : x.s with
  | [] =>
    have proof : x.s = [] := h
    f x proof
  | _ => false

[Adam Topaz]

no need for :face_palm: I think most people don't know that this is an option... it's not used very often.

[Bhavik Mehta]

Perhaps I'm missing it, but I don't think this is documented in TPiL or in FPiL? I've also needed this in practice, so I believe it's worth being documented somewhere

[Patrick Massot]

This will certainly be in the reference manual at some point. @David Thrane Christiansen

[Bhavik Mehta]

It's not in the Match expressions section of the reference manual