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: