Problem with custom infix syntax

Stream: new members

[Zhang Qinchuan]

I'm reading Meta In Lean4. At the begining of chapter 5, it gives the following example of custom infix syntax:

infixl:60 " ⊕ " => fun l r => (!l && r) || (l && !r)

When I try to evaluate true ⊕ false ⊕ true using the following code:

infixl:60 " ⊕ " => fun l r => (!l && r) || (l && !r)
#eval true ⊕ false ⊕ true

Lean tries to interpret true ⊕ false ⊕ true as Sum true (false ⊕ true) rather than fun l r => .. and hence lean prints the following error message:

application type mismatch
  Sum true
argument
  true
has type
  Bool : Type
but is expected to have type
  Type ?u.661 : Type (?u.661 + 1)

If I change infixl to infixr, then true ⊕ false ⊕ true is evaluated to false which is expected.

Why in the infixl case, lean failed to evaluate true ⊕ false ⊕ true?

[Kevin Buzzard]

Is that notation already being used to mean something else? If so then you're asking for trouble

[Zhang Qinchuan]

Kevin Buzzard said:

Is that notation already being used to mean something else? If so then you're asking for trouble

Sum in Lean4 use ⊕. But the parameters of Sum are α : Type u and β : Type v:

inductive Sum (α : Type u) (β : Type v) where
  | inl (val : α) : Sum α β
  | inr (val : β) : Sum α β

As true, false are Bool, I am confused that Lean tries to interpret true ⊕ false ⊕ true as a Sum.

[Kyle Miller]

It seems that you have to match the parsing exactly if you are going to overload notation. This works:

infixr:30 " ⊕ " => fun l r => (!l && r) || (l && !r)
#eval true ⊕ false ⊕ true

[Zhang Qinchuan]

Kyle Miller said:

It seems that you have to match the parsing exactly if you are going to overload notation. This works:

infixr:30 " ⊕ " => fun l r => (!l && r) || (l && !r)
#eval true ⊕ false ⊕ true

It is sufficient to change infixl to infixr. The following code work well:

infixr:60 " ⊕ " => fun l r => (!l && r) || (l && !r)
#eval true ⊕ false ⊕ true

I just wonder why infixl did not work.