Unexpected equation compiler behaviour

Stream: general

[Chris Hughes]

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]

one is a variable in the first definition

[Reid Barton]

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

[Patrick Massot]

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]

one is a variable in the first definition

how does succ zero define a variable?

[Patrick Massot]

it doesn't

[Kenny Lau]

then why does it work?

[Chris Hughes]

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

[Patrick Massot]

Try replacing one by three in the def of is_even

[Patrick Massot]

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

[Kenny Lau]

oh!