Introducing an embedding relation between two sorts may cause function
symbols to become related by the overloading relation, so that values
of terms become equated when the terms are identical up to embedding.
A subsort declaration SUBSORT-DECL declares all the sorts in
the list SORT+, as well as their embedding in the specified
SORT. The same sort may not occur more than once in each
SUBSORT-DECL. A SUBSORT-DECL is well-formed only when
it does not cause mutual or cyclic embeddings.
SIG-DECL ::= ... | SUBSORT-DECL
SUBSORT-DECL ::= subsort-decl SORT+ SORT
By specifying an isomorphism declaration ISO-DECL, each sort in
the list SORT+ is embedded in all the other sorts in that list,
thus allowing mutual and cyclic embedding, which correspond to
isomorphisms between the carrier sets. An ISO-DECL is
well-formed only when there are at least two SORT components in
the list SORT+.
SIG-DECL ::= ... | ISO-DECL
ISO-DECL ::= iso-decl SORT+
CoFI
Document: CASL/Summary-v0.97 --Version 0.97-- 20 May 1997.
Comments to cofi-language@brics.dk