**Go up to** 4.2.1 Atomic Formulae

#### 4.2.1.1 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