6 Other examples of SORT-ITEM

6.1 Example for SORT-DECL, SUBSORT-DECL and ISO-DECL

spec

NAT =

sorts

Nat;
Zero,Pos<Nat

 %% Zero and Pos are subsorts of Nat

Weight = Nat

 %% Weight is an isosort of Nat

...

end

6.2 Example for SUBSORT-DEFN

spec

NAT_WITH_ODD =

sorts

Nat;

...

op

odd__:pred(Nat)

axioms

¬ odd zero

forall x:Nat.

odd(suc x) <=> ¬ odd x

sort

Odd = {n:Nat.odd n}

 %% Odd is a subsort of Nat

end