cases_on bytecode

Stream: new members

[Mateusz Zugaj]

prelude
inductive nat
| zero : nat
| succ : nat → nat
definition add (n : nat) (m: nat) : nat :=
nat.rec n (λ k nk, nat.succ nk) m

[Mateusz Zugaj]

I get a warning

[Mateusz Zugaj]

failed to generate bytecode for 'add'
unknown declaration 'nat.cases_on'

[Mateusz Zugaj]

What's going on?

[Mateusz Zugaj]

If nat.cases_on is not defined automatically, then why it's needed?

[Reid Barton]

nat has special support in the interpreter (to use GMP instead of the unary representation). So I'm not entirely surprised that replacing it causes interpreter-related issues. I don't know how to explain this specifically, though; maybe look at how nat is set up in the core library?

[Kevin Buzzard]

Changing nat to mat gives the same error