Zulip Chat Archive

Stream: new members

Topic: cases_on bytecode


view this post on Zulip 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

view this post on Zulip Mateusz Zugaj (Jul 09 2020 at 10:00):

I get a warning

view this post on Zulip Mateusz Zugaj (Jul 09 2020 at 10:00):

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

view this post on Zulip Mateusz Zugaj (Jul 09 2020 at 10:00):

What's going on?

view this post on Zulip Mateusz Zugaj (Jul 09 2020 at 10:03):

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

view this post on Zulip 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?

view this post on Zulip 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