Overloading operators

Stream: general

[Mai]

Is there a reason certain operators like - (Neg) are overloadable, but others like ! and ¬ are not?

[Violeta Hernández]

Because in mathematics the meaning of - is entirely dependent on what structure you're talking about, while ¬ is something you only ever do to a proposition.

[Violeta Hernández]

Though perhaps docs#Compl is worth mentioning

[Violeta Hernández]

It's perhaps misleading to think of Lean operators as overridable in the sense that operators in other languages are. Lean doesn't really have the notion of an operator, it only has infix or prefix or postfix notations. Some of these refer to a typeclass, others refer to one specific function on one specific type.

[Edward van de Meent]

note also that lean is able to parse amgibuous syntax, meaning it might be possible for you to add a (scoped) notation locally overriding the syntax (because hopefully only one version ever successfully elaborates)

[Yury G. Kudryashov]

See also docs#Complement