+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+
inductive True: Prop \def
I : True.
qed.
-let rec plus n m : nat \def
+let rec plus n m \def
match n with
[ O \Rightarrow m
| (S p) \Rightarrow S (plus p m) ].
intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
qed.
-let rec times n m : nat \def
+let rec times n m \def
match n with
[ O \Rightarrow O
| (S p) \Rightarrow (plus m (times p m)) ].
simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
qed.
-let rec minus n m : nat \def
- [\lambda n:nat.nat] match n with
+let rec minus n m \def
+ match n with
[ O \Rightarrow O
| (S p) \Rightarrow
[\lambda n:nat.nat] match m with
apply le_S_n.assumption.
qed.
-let rec leb n m : bool \def
- [\lambda n:nat.bool] match n with
+let rec leb n m \def
+ match n with
[ O \Rightarrow true
| (S p) \Rightarrow
[\lambda n:nat.bool] match m with