have giving error

Stream: Berkeley Lean Seminar

[Thomas Browning]

the expression

have h : a * b = a * b → a = a,

gives no errors but the expression

have h' : a * b = a * b → a * b = a * b,

gives an error at the third multiplication symbol. Why is this and how can it be avoided?

[Patrick Lutz]

actually, even looking at the state after your first have, it's not what I expected

[Kyle Miller]

Shouldn't it be := rather than : ?

[Patrick Lutz]

the : is saying the type of h

[Patrick Lutz]

for instance have h : (\forall a : \N), (\forall b : \N), a*b = a*b \to a*b = a*b works and gives what you would expect

[Thomas Browning]

I thought that it would function like

have h : 0=0,

(which functions as expected)

[Thomas Browning]

I thought that it would function like

have h : a=a,

(which functions as expected)

[Patrick Lutz]

might be worth asking in the new members stream

[Patrick Lutz]

have h : a = b, also works as expected. As does have h : a = b \and a = b,

[Patrick Lutz]

btw, I think they typically like you to give a mwe (minimum working example) in the other streams

[Patrick Lutz]

to report back what was said in the new members stream, apparently there's an insane bug where when you use the letter a as a variable in a have statement, Lean implicitly adds a universal quantifier (basically)

[Kevin Buzzard]

The last time this bug was discussed, fixing it involved the impossible act of editing core Lean. Now there's a fork and this bug is fixable.