LP, the Larch Prover -- Infix, prefix, and postfix operators

LP allows users to declare symbols that can be used for infix, postfix, and prefix notations. Users can declare a simple operator (i.e., a <simpleOp>) for such use by decorating it with one or two markers (__) to indicate the location(s) of its arguments. For example, the declarations

declare operators 
  __+__, __\mod__: Nat, Nat -> Nat   % infix operators
  -__:             Nat      -> Nat   % prefix operator
  __!:             Nat      -> Nat   % postfix operator
  ..

allow the use of infix (e.g., (x + 1) \mod n), prefix (e.g., ~p and -x), and postfix (e.g., 3!) notations. Users can also declare a selection operator for use in postfix notations. For example, the declaration

declare operator __.first: Queue -> Element

allows the use of postfix notations such as q.first. See operator.