Prev Up
Go backward to 2.3.3.3 Definedness
Go up to 2.3.3 Atomic Formulae

2.3.3.4 Equations

  EXISTL-EQUATION  ::= existl-equation TERM TERM
  STRONG-EQUATION  ::= strong-equation TERM TERM

An existential equation EXISTL-EQUATION is written:

T1  =e=  T2
The sign displayed as an `e' over a `=' in LaTeX is input as `=e='.

A strong equation is written:

T1 = T2

An existential equation holds when the values of the terms are both defined and equal; a strong equation holds also when the values of both terms are undefined (thus the two forms of equation are equivalent when the values of both terms are always defined).

An equation is well-sorted if there is a sort such that both terms are well-sorted for that sort. It then expands to the corresponding existential or strong equation on the fully-qualified expansions of the terms for that sort.


CoFI Document: CASL/Summary --Version 0.99-- 21 April 1998.
Comments to cofi-language@brics.dk

Prev Up