Go up to 4.2.1 Atomic Formulae Membership

      MEMBERSHIP ::= membership TERM SORT

A membership formula is written:

T e s
The sign displayed as the set-membership symbol in LaTeX is input as `in'.

It is well-sorted if the term T is well-sorted for a supersort s' of the specified sort s. It expands to an application of the pre-declared predicate symbol for testing s' values for membership in the embedding of s.

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk