definition plus : nat \to nat \to nat \def
-let rec plus (n,m) \def
+let rec plus n m \def
match n with
[ O \Rightarrow m
| (S p) \Rightarrow S (plus p m) ]
qed.
definition times : nat \to nat \to nat \def
-let rec times (n,m) \def
+let rec times n m \def
match n with
[ O \Rightarrow O
| (S p) \Rightarrow (plus m (times p m)) ]
qed.
definition minus : nat \to nat \to nat \def
-let rec minus (n,m) \def
+let rec minus n m \def
[\lambda n:nat.nat] match n with
[ O \Rightarrow O
| (S p) \Rightarrow
qed.
definition leb : nat \to nat \to bool \def
-let rec leb (n,m) \def
+let rec leb n m \def
[\lambda n:nat.bool] match n with
[ O \Rightarrow true
| (S p) \Rightarrow