failed to generate bytecode error

Stream: general

[Gihan Marasingha]

I'm writing special cases of eliminators for pedagogical purposes. The following definition of myseq results in the the warningfailed to generate bytecode for 'myseq' code generation failed, VM does not have code for 'nat.seq'. What's going on? This is Lean 3.30.

lemma nat.seq (n : ℕ) (h₀ : ℕ) (h₁ : ∀ (k : ℕ), ℕ → ℕ) : ℕ := nat.rec_on n h₀ h₁

def myseq (n : ℕ) : ℕ := nat.seq n 6 (λ k seq_k, 5 + 2 * seq_k)

[Eric Rodriguez]

nat.seq should be a def

[Gihan Marasingha]

Thanks very much!

[Kevin Buzzard]

Can we edit that error somehow? Sometimes Lean gives you a rare error and then says something helpful like "possible fix:try tactic.unfreeze_local_instances". Can we have a "possible fix: Lint your file by writing #lint at the bottom, to detect any lemmas which should have been definitions."

[Kevin Buzzard]

Gihan is by no means the first person to ask this question.

[Eric Wieser]

I've changed these messages before - you can just search the lean source code for some snippet of the message, and then PR a rewording

[Eric Wieser]

"perhaps it is a lemma but was intended to be a def" would probably be a good addition to the error message here

[Gihan Marasingha]

I'm now getting an error "eliminator" elaborator failed to compute the motive when the definition nat.rec_on' below is in a section. Everything's fine if the definition is outside a section. What's happening? Is the only fix not to define nat.rec_on' within a section?

section foo

universe u

@[elab_as_eliminator]
def nat.rec_on' {C : ℕ → Sort u} (n : ℕ) (h₀ : C 0) (h₁ : ∀ (k : ℕ), C k → C k.succ) : C n :=
nat.rec_on n h₀ h₁

def seq (n : ℕ) : ℕ := nat.rec_on' n 6 (λ k seq_k, 5 + 2 * seq_k)

end foo

Edit: I see now that this works fine if at most one of the definitions nat.rec_on' and seq are in the section foo!

Edit edit: Now I see everything is fine as long as universe u is declared outside the section. I probably need to refer back to TPIL.

[Eric Wieser]

This looks like it could be a bug - could you post as separate mwes the versions that do and do not work?

[Gihan Marasingha]

@Eric Wieser the above does not work, the following does work:

universe u

section foo

@[elab_as_eliminator]
def nat.rec_on' {C : ℕ → Sort u} (n : ℕ) (h₀ : C 0) (h₁ : ∀ (k : ℕ), C k → C k.succ) : C n :=
nat.rec_on n h₀ h₁

def seq (n : ℕ) : ℕ := nat.rec_on' n 6 (λ k seq_k, 5 + 2 * seq_k)

end foo