LP, the Larch Prover -- Bracketed operators


LP allows users to employ bracketed notations for operators. These notations consist of opening and closing symbols interspersed with arguments (in terms) or markers (in declarations). LP recognizes the following opening and closing symbols: For example, the declarations
declare operators
  {}:                         -> Set
  {__}:      Nat              -> Set
  __[__]:    Array, Nat       -> Nat
  __[__,__]: Matrix, Nat, Nat -> Nat
  [__]__:    Nat, Matrix      -> Array
  ..
enable the following notations: