Prev Up Next
Go backward to E.3.2 Num_Monoid
Go up to E.3 Architectural Specifications
Go forward to E.3.4 Add_Num_Efficiently

E.3.3 Add_Num

spec
Add_Num =
 
Num and Num_Monoid
then
 
axiom
forall x,y : Num · x+succ(y) = succ(x+y)
end

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk

Prev Up Next