Zulip Chat Archive

Stream: general

Topic: Unexpected equation compiler behaviour


Chris Hughes (Jul 12 2018 at 13:44):

Is this a bug?

inductive xnat
| zero : xnat
| succ : xnat  xnat

open xnat

def one := succ zero

def is_even : xnat  bool
| zero := tt
| one := ff -- works, but shouldn't

def is_even : xnat  bool
| zero := tt
| (succ zero) := ff -- error, as expected

Mario Carneiro (Jul 12 2018 at 13:47):

one is a variable in the first definition

Reid Barton (Jul 12 2018 at 13:47):

one doesn't have the pattern attribute, so... ^

Patrick Massot (Jul 12 2018 at 15:26):

That's a nice one! Note that:

inductive xnat
| zero : xnat
| succ : xnat  xnat

open xnat

def one := succ zero

def is_even : xnat  bool
| zero := tt
| one := ff -- works, as it should

example : is_even one := rfl -- fails, as it should

Kenny Lau (Jul 12 2018 at 15:28):

one is a variable in the first definition

how does succ zero define a variable?

Patrick Massot (Jul 12 2018 at 15:28):

it doesn't

Kenny Lau (Jul 12 2018 at 15:28):

then why does it work?

Chris Hughes (Jul 12 2018 at 15:28):

one doesn't refer to the def it's the same as writing n

Patrick Massot (Jul 12 2018 at 15:28):

Try replacing one by three in the def of is_even

Patrick Massot (Jul 12 2018 at 15:29):

Lean is guaranteed to be correct, not to be non-confusing

Kenny Lau (Jul 12 2018 at 15:30):

oh!


Last updated: Dec 20 2023 at 11:08 UTC