From 7482cad729419e16abb0c68ea04ec13513996988 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jul 2005 13:09:34 +0000 Subject: [PATCH] added test for assumption --- helm/matita/tests/assumption.ma | 38 +++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 helm/matita/tests/assumption.ma diff --git a/helm/matita/tests/assumption.ma b/helm/matita/tests/assumption.ma new file mode 100644 index 000000000..711e35cf0 --- /dev/null +++ b/helm/matita/tests/assumption.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/tests/assumption". + +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias num (instance 0) = "natural number". +alias symbol "and" (instance 0) = "logical and". +alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "plus" (instance 0) = "natural plus". + + +theorem stupid: + \forall a: 0 = 0. + \forall b: 3 + 2 = 5. + \forall c: (\lambda x:nat.x) 3 = 3. + 0=0 \land 3 + 2 = 5 \land 3 = 3. +intros. +split. +split. +clear H2. clear H1. +assumption. +clear H. +assumption. +assumption. +qed. + -- 2.39.2