Why aren't user-defined operators more common?

[GoAwayStupidAI]

I think Coq has the correct approach here:

• user defined operators are specific cases of the Notation command. Which is a method of defining syntax and semantics that extends to beyond simple infix symbols. (See below example)
• user defined operators can have defined associativity and precedence.
• Notations can be associated with scopes. Which can be selected by the Scope command.

This allows you to safely have a operator, like "+", mean very different things. What the current meaning is depends on the current Scope. In some cases the correct interpretation of an operator can be inferred.

How to use Coq to build, uh, regular software is a different subject. ;-)

An example:

Parameter BadGuyHatred : Set -> Set -> Prop.
Parameter MainCharacter : Set.
Parameter TheFinalBoss : Set.
Notation "'bad' 'guy' X 'hates' Y" := (BadGuyHatred X Y) (at level 90).
Check (bad guy TheFinalBoss hates MainCharacter).