operator overload issue

Stream: new members

[Kevin Sullivan]

Do you know offhand why overloading => causes the following failure (Lean 3)?

#check tt = tt    -- Prop
notation (name := pImp) e1 => e2 := pBinOp opImp e1 e2
#check tt = tt    -- INVALID EXPRESSION

Changing = to == (eq to heq) makes the error go away, as does changing the operator from => to ==>

[Mario Carneiro]

You didn't put backquotes around the => operator, so it's probably being lexed as two tokens. That is, you are actually defining e1 = > e2 and this breaks the behavior of the = operator

[Mario Carneiro]

indeed, this works:

#check tt = tt    -- Prop
notation (name := pImp) e1 ` => ` e2 := pBinOp opImp e1 e2
#check tt = tt    -- ok

[Kevin Sullivan]

Mario Carneiro said:

indeed, this works:

#check tt = tt    -- Prop
notation (name := pImp) e1 ` => ` e2 := pBinOp opImp e1 e2
#check tt = tt    -- ok

Yeah, thanks. I was just adding them when you replied (head lowered).

[Mario Carneiro]

alternatively you can declare => as a token beforehand

#check tt = tt    -- Prop
precedence `=>`:50
notation (name := pImp) e1 => e2 := e1 > e2
#check tt = tt    -- ok