CASL/Summary-v0.99-draft -- 2.3.3.3 Definedness

Go backward to 2.3.3.2 Predicate Application
Go up to 2.3.3 Atomic Formulae
Go forward to 2.3.3.4 Equations

2.3.3.3 Definedness

  DEFINEDNESS      ::= definedness TERM

A definedness formula is written:

def T

It is well-sorted when the term is well-sorted for some sort. It then expands to a definedness assertion on the fully-qualified expansion of the term.

CoFI Document: CASL/Summary-v0.99-draft --DRAFT Version 0.99-- 25 March 1998.
Comments to cofi-language@brics.dk