search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
43 stars 15 forks source link

Postfix precedence issues #114

Closed gebner closed 2 years ago

gebner commented 2 years ago 
postfix:1025 "ˣ" => Units

instance : Coe (α)ˣ α :=
                --^ expected ')'

It works fine if the precedence is lowered to 1024.

digama0 commented 2 years ago

1024 is the precedence of application, so it seems important to use 1025 here. Or has the precedence of application changed?

Kha commented 2 years ago

For the standard precedences see https://github.com/leanprover/lean4/blob/09866967589096c36c05762dbd02e367fbfebf8b/src/Init/Notation.lean#L23-L25; max should be sufficient here. postfix:1025 is problematic in Lean 4 because it expands to syntax:1025 term:1025 : term, and not even parentheses fit into the 1025-hole.

gebner commented 2 years ago

Apparently, postfix:1024 works in Lean 4 and A Bˣ parses as A (Bˣ). So let's just truncate it to 1024. #115