simp and matching def

Stream: new members

[Liam O'Connor]

If I have a definition which does some matching,like :

def foo  : List α → Nat
  | nil       => 0
  | cons _ as => 1

(just as an example)

If I declare this @[simp] then simp will rewrite this into an ugly match expression in my goals. But if I don't declare it @[simp] then it won't even simplify foo nil to 0. Is there a way to add only the matches as equations to the simp set (essentially Isabelle's fun behaviour)? (without writing them out as separate lemmas)

[Eric Wieser]

This is lean4#2042 I think

[Liam O'Connor]

I'm a little surprised that this simplifier behaviour isn't supported by default. Isabelle's simp works this way and IIRC lean3's did as well.

[Liam O'Connor]

For now I'm working around this by writing a series of lemmas for each equation and adding them to the simpset, but surely there is a better way? I'm basically writing every definition twice