datatype int=Zero|Succ of int|Pred of int;
Zero:int;
Succ:int->int;
Pred:int->int;


fun add(Zero,n)=n
 |  add(Succ(m),n)=Succ(add(m,n)) 
 |  add(Pred(m),n)=Pred(add(m,n));

fun IsZero(x)=(x=Zero);

fun IsPos(Zero)=false
 |  IsPos(Succ(Zero))=true
 |  IsPos(Pred(Zero))=false;

fun Norm(Zero)=Zero
 |  Norm(Succ(x))=Succ(Norm(x))
 |  Norm(Pred(x))=Pred(Norm(x))
 |  Norm(Succ(Succ(x)))=Norm(Succ(Norm(Succ(x))))
 |  Norm(Pred(Pred(x)))=Norm(Pred(Norm(Pred(x))))
 |  Norm(Succ(Pred(x)))=Norm(x)
 |  Norm(Pred(Succ(x)))=Norm(x);

add(Pred(Succ(Succ(Zero))),Succ(Succ(Succ(Zero))));

(*
val Succ (n:int)=n+1;


signature NumMapping = sig
 val Zero:int
 val add:(int * int)->int
end;

structure NumMap : NumMapping = int;
*)