1 inductive pos: Set \def
9 inductive int: Set \def
10 | positive: nat \to int
11 | negative : nat \to int.
13 inductive empty : Set \def .
15 let rec pos2nat (x:pos) : nat \def
17 [ one \Rightarrow (S O)
18 | (next z) \Rightarrow S (pos2nat z)].
20 let rec nat2int (x:nat) :int \def
22 [ O \Rightarrow positive O
23 | (S z) \Rightarrow positive (S z)].
29 let rec plus (x,y:int) on x : int \def
31 [ (positive n) \Rightarrow x
32 | (negative z) \Rightarrow y].
34 theorem a: plus O one.