precedence paradox

Stream: new members

[Asei Inoue]

-- I think `160` is higher than precedence of `=`
infixl:160 " ⊕ " => xor

-- but this raise an error...
/-
application type mismatch
  Sum true
argument
  true
has type
  Bool : Type
but is expected to have type
  Type ?u.1547 : Type (?u.1547 + 1)
-/
#guard true ⊕ true = false

-- no error
#guard (true ⊕ true) = false

[Asei Inoue]

TPiL says the precedence of = is 50!

[Yaël Dillies]

infixl:160 " newnotation " => xor

-- Both work
#guard true newnotation true = false
#guard (true newnotation true) = false

[Yaël Dillies]

The issue is that your notation is conflicting with the docs#Sum notation which has precedence 30

[Asei Inoue]

@Yaël Dillies Thank you!

However, if the symbols are overlapped, it would be nice to get some warning when the infixl command is executed. Is there any direct way for the command to know if the symbols are overlapped?

[Kyle Miller]

You can set a higher priority on your new notation to override Sum's notation

[Kyle Miller]

infixl:160 (priority := high) " ⊕ " => xor

[Kyle Miller]

I don't know of any command to get warnings about overlapping notations.

[Asei Inoue]

@Kyle Miller Thank you!! but It is sad that I don't know how to know with Lean commands whether the notation is conflicting or not.

[Kyle Miller]

At least you run into issues quickly. The "application type mismatch" is giving a hint that it's conflicting with some notation having to do with Sum, which gives you some information about what to search for in the source code.

[Asei Inoue]

By the way, is it possible to get the notation precedence without having to go and look at the definitions or write tests?

[Yaël Dillies]

It was possible in Lean 3, but I don't think it is in Lean 4?

[Kyle Miller]

I'm not sure. There's #help term but it doesn't show precedences (and it doesn't show very much information about operators defined using infix)

[Kyle Miller]

In principle it's possible of course.

What I do for now is right click on notations and go to their definitions.

[Notification Bot]

Asei Inoue has marked this topic as resolved.

[Asei Inoue]

Thank you all!

[Notification Bot]

Asei Inoue has marked this topic as unresolved.

[Asei Inoue]

still error...?

infix:160 (priority := high) " ⊕ " => xor

/-
application type mismatch
  Sum true
argument
  true
has type
  Bool : Type
but is expected to have type
  Type ?u.3535 : Type (?u.3535 + 1)
-/
#guard true ⊕ true = false

[Kyle Miller]

Sorry, I didn't test it. It seems that you can't override it if you change anything about the notation.

[Asei Inoue]

...Is it not possible to set it so that xor is always called when ⊕ is used against a Bool term?

[Kyle Miller]

If you make the precedence be 30 you can make it be xor, but then you need to remember to use parentheses.

[Kyle Miller]

Here's another way to override the meaning of a preexisting notation instead of using priorities:

macro_rules | `($x ⊕ $y) => `(xor $x $y)

[Asei Inoue]

oh, that's nice. but why this works? Is macro_rules expanded before infix?

macro_rules | `($x ⊕ $y) => `(xor $x $y)

#guard true ⊕ true = false
#guard true ⊕ false = true
#guard false ⊕ true = true
#guard false ⊕ false = false

[Kyle Miller]

The infix command does three things: it defines the syntax, it creates a macro_rules for expanding the syntax, and it (tries to) create an app_unexpander for pretty printing.

Macro rules are considered in reverse order of definition. Adding your own macro rules means it overrides the one that came from infix.

[Asei Inoue]

@Kyle Miller Thank you! Indeed, using macro_rules seems to disable the Sum notation. Override.

macro_rules | `($x ⊕ $y) => `(xor $x $y)

#guard true ⊕ true = false
#guard true ⊕ false = true
#guard false ⊕ true = true
#guard false ⊕ false = false

#check_failure Nat ⊕ Fin 2

[Notification Bot]

Asei Inoue has marked this topic as resolved.

[Notification Bot]

Asei Inoue has marked this topic as unresolved.

[Asei Inoue]

@Kyle Miller I forgot to ask an important question ...

why this does not work?

infix:160 (priority := high) " ⊕ " => xor

#guard true ⊕ true = false

[Asei Inoue]

priority of notation of Sum is not set as priority := high

@[inherit_doc] infixr:30 " ⊕ " => Sum

[Asei Inoue]

I wonder priority cannot override notation...?

[Kyle Miller]

My guess is that having the same notation with different precedences is confusing the parser. The priority as far as I know is only used when disambiguating after a successful parse. Both the Sum and xor notations can parse successfully, but they have completely different parse trees, and I don't know what happens in that case. Experimentally, we see in your example that it goes back to interpreting true ⊕ true = false as Sum true (Eq true false) rather than Eq (xor true true) false. However, if you do true ⊕ true alone it respects the priority and is interpreted as xor true true.