code generator does not support recursor yet

Stream: lean4

[Elisabeth Bonnevier]

I am trying to learn Lean and I have written this code:

inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat

def nat_to_mynat (n : Nat) : MyNat := by
  induction n with
  | zero => exact MyNat.zero
  | succ _ m => exact (MyNat.succ m)

but I get the error message "code generator does not support recursor 'Nat.rec' yet, consider using 'match ... with' and/or structural recursion" on nat_to_mynat. Why?
I am using version 4.0.0-nightly-2022-10-18, commit faa612e7b79a
Please forgive me if I am missing something obvious here

[Eric Wieser]

Can you update to a version that's 3 months newer?

[Elisabeth Bonnevier]

I'll try :smiling_face: just a moment...

[Elisabeth Bonnevier]

So I just ran elan update and now I have version 4.0.0-nightly-2023-01-06. Still the same error message :cry:

[Reid Barton]

This hasn't changed yet. You can use noncomputable, or use the equation compiler/match.

[Reid Barton]

We mostly don't use tactics to write definitions (as opposed to proofs)

[Elisabeth Bonnevier]

Reid Barton said:

We mostly don't use tactics to write definitions (as opposed to proofs)

I see, thanks for the tip!

[Elisabeth Bonnevier]

Reid Barton said:

This hasn't changed yet. You can use noncomputable, or use the equation compiler/match.

Now I wrote

def nat_to_mynat (n : Nat) : MyNat :=
  match n with
  | Nat.zero => zero
  | Nat.succ m => (succ (nat_to_mynat m))

and it works :partying_face: Thanks for the newbie help!

[Henrik Böving]

Reid Barton said:

This hasn't changed yet. You can use noncomputable, or use the equation compiler/match.

There is someone who very ocasionally visits the compiler meetings that wants to work on this but apart from that there is no plans to change it at all in the close future.