-
Notifications
You must be signed in to change notification settings - Fork 6
sort
Norbert Preining edited this page Oct 6, 2017
·
1 revision
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.
[ 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
.
CafeOBJ Reference Manual (c) 2015-2018 CafeOBJ Development Team