diff --git a/doc/notation.md b/doc/notation.md index 8f6c544db0..d1e1b8203b 100644 --- a/doc/notation.md +++ b/doc/notation.md @@ -7,7 +7,7 @@ overloading existing) prefix, infix, and postfix operators. infixl:65 " + " => HAdd.hAdd -- left-associative infix:50 " = " => Eq -- non-associative infixr:80 " ^ " => HPow.hPow -- right-associative -prefix:100 "-" => Neg.neg +prefix:75 "-" => Neg.neg # set_option quotPrecheck false postfix:max "⁻¹" => Inv.inv ``` @@ -26,7 +26,7 @@ can make this more precise by looking at what the commands above unfold to: notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs notation:50 lhs:51 " = " rhs:51 => Eq lhs rhs notation:80 lhs:81 " ^ " rhs:80 => HPow.hPow lhs rhs -notation:100 "-" arg:100 => Neg.neg arg +notation:75 "-" arg:75 => Neg.neg arg # set_option quotPrecheck false notation:1024 arg:1024 "⁻¹" => Inv.inv arg -- `max` is a shorthand for precedence 1024 ``` diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index d2987cef6a..dd5ea506b3 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -263,7 +263,7 @@ syntax (name := rawNatLit) "nat_lit " num : term @[inherit_doc] infixl:75 " >>> " => HShiftRight.hShiftRight @[inherit_doc] infixr:80 " ^ " => HPow.hPow @[inherit_doc] infixl:65 " ++ " => HAppend.hAppend -@[inherit_doc] prefix:100 "-" => Neg.neg +@[inherit_doc] prefix:75 "-" => Neg.neg @[inherit_doc] prefix:100 "~~~" => Complement.complement /-!