and |
logical conjunction |
as |
introduces a local name for a relation imported from another module |
def |
begins the declaration of a relation |
else |
separates the two branches of a conditional expression |
end |
ends a conditional expression or a module |
entity |
begins the declaration of an entity type (deprecated) |
exists |
the existential quantifier |
false |
boolean constant (the empty relation {}) |
for |
an alternative form of relational abstraction |
forall |
the universal quantifier |
from |
a variant of inverse relational abstraction |
ic |
begins the declaration of an integrity constraint |
if |
begins a conditional expression |
iff |
boolean equivalence |
implies |
logical implication |
in |
binds a variable to the elements of a set of singletons |
module |
begins the declaration of a module |
not |
logical negation |
or |
logical disjunction |
then |
separates the condition and the first branch of a conditional expression |
true |
boolean constant (the singleton relation {()}) |
use |
begins the list of names imported from another module |
where |
binds variables to sets of values that satisfy a formula |
with |
begins the declaration of imports from another module |
xor |
logical “exclusive or” |