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:

opening symbols: [, {, \(, \<
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:

empty set: {}
singleton set: {x}
element of an array: a[n]
element of a matrix: m[1, 2]
slice of a matrix: [1]m