Match with motive syntax

Stream: lean4

[Leni Aniva]

Executing

#print Nat.zero_add

gives

protected theorem Nat.zero_add : ∀ (n : Nat), 0 + n = n :=
fun x =>
  Nat.brecOn x fun x f =>
    (match (motive := ∀ (x : Nat), Nat.below x → 0 + x = x) x with
      | 0 => fun x => rfl
      | n.succ => fun x => congrArg Nat.succ x.fst.fst)
      f

Is the match (motive := ...) x with syntax sugar for something else? What does it do?

[Joachim Breitner]

Try set_option pp.match false

[Max Nowak 🐉]

“match” is not a primitive in Lean, instead eliminators are, which is what match elaborates to. Every inductive type gets one eliminator, which you can find by appending “rec”, for example List.rec