The following example illustrates a complete basic specification:
Notice that the second line above declares suc : Nat -> Pos and pre : Pos -> Nat. The subsequent declaration of pre : Nat ->? Nat allows terms where pre is applied to an argument that is of sort Nat but not of sort Pos--such terms can be perfectly meaningful, e.g., pre(pre(suc(suc(0)))).
- free types
Nat ::= 0 | sort Pos; Pos ::= suc(pre:Nat) - op
- pre : Nat ->? Nat
- axioms
¬ def pre(0);
forall n:Nat · pre(suc(n)) = n
- pred
- even__ : Nat
- var
- n:Nat
- ·
- even 0
- ·
- even suc(n) <=> ¬ even n
Further examples may be found in later sections, and in the appendices of the CASL Summary [4].