## Stream: new members

### Topic: cases_on bytecode

#### Mateusz Zugaj (Jul 09 2020 at 10:00):

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


I get a warning

#### Mateusz Zugaj (Jul 09 2020 at 10:00):

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


What's going on?

#### Mateusz Zugaj (Jul 09 2020 at 10:03):

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

#### Reid Barton (Jul 09 2020 at 12:02):

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 (Jul 09 2020 at 14:47):

Changing nat to mat gives the same error

Last updated: May 14 2021 at 03:27 UTC