sort

sort declaration

CafeOBJ supports two kind of sorts, visible and hidden sorts. Visible sorts are introduced between [ and ], while hidden sorts are introduced between *[ and ]*.

  [ Nat ]
  *[ Obs ]*

Several sorts can be declared at the same time, as in [ Nat Int ].

Since CafeOBJ is based on order sorting, sorts can form a partial order. Definition of the partial order can be interleaved by giving

  [ <sorts> < <sorts> ]

Where sorts is a list of sort names. This declaration defines an inclusion relation between each pair or left and right sorts.

Example

  [ A B , C D < A < E, B < D ]

defines five sorts A,...,E, with the following relations: C < A, D < A, A < E, B < D.