No support for code generation

Stream: lean4

[Uranus Testing]

inductive Path (α : Type u) : α → α → Type u
| refl : Path α a a

-- error:
-- code generator does not support recursor 'Path.rec' yet,
-- consider using 'match ... with' and/or structural recursion
def Path.symm (p : Path α a b) : Path α b a :=
by { induction p; apply Path.refl }

Why?

[Leonardo de Moura]

As the error message suggests, this has not been implemented.
The compiler only has support for casesOn recursor.
Note that the following works

inductive Path (α : Type u) : α → α → Type u
| refl : Path α a a

def Path.symm (p : Path α a b) : Path α b a :=
by { cases p; apply Path.refl }

The casesOn recursor is equivalent to the rec one for nonrecursive types.
For recursive types, we strongly encourage users to write recursive definitions. It is easier to write, and the generated code is more efficient.

[Uranus Testing]

Types of Path.rec and Path.casesOn are very similar:

#check Path.rec
-- {α : Type u_2} →
--  {motive : (a a_1 : α) → Path α a a_1 → Sort u_1} →
--    ({a : α} → motive a a Path.refl) → {a a_1 : α} → (t : Path α a a_1) → motive a a_1 t

#check Path.casesOn
-- {α : Type u_2} →
--   {motive : (a a_1 : α) → Path α a a_1 → Sort u_1} →
--     {a a_1 : α} → (t : Path α a a_1) → ({a : α} → motive a a Path.refl) → motive a a_1 t

So what’s the difference?

[Uranus Testing]

Ah, missed the part about “The casesOn recursor is equivalent to the rec one for nonrecursive types.”