![Next](http://www.daimi.aau.dk/images/next.xbm)
Go backward to E.1.2 MONOID
Go up to E.1 Specifications from the Bremen Proposal
Go forward to E.1.4 SIG1
E.1.3 NAT
- spec
- NAT =
- free
-
- {
-
- sorts
- Nat;
Zero,Pos < Nat
- ops
- zero : Zero;
suc__ : Nat -> Pos
}
- then
-
- op
- pre__ : Pos -> Nat
- var
- x : Nat
- ·
- pre(suc x)=x
- then local
-
- pred
- odd__ : Nat
- var
- x : Nat
- ·
- ¬ odd zero
- ·
- odd(suc x) <=> ¬ odd x
- within
-
- sort
- Odd = { n:Nat · odd n }
CoFI
Document: CASL/Summary --Version 0.99-- 21 April 1998.
Comments to cofi-language@brics.dk
![Next](http://www.daimi.aau.dk/images/next.xbm)