From b267219c702ccf60744f8044291ed9da4e80f7fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 7 Jul 2005 11:02:44 +0000 Subject: [PATCH] added test for elim --- helm/matita/tests/elim.ma | 41 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 helm/matita/tests/elim.ma diff --git a/helm/matita/tests/elim.ma b/helm/matita/tests/elim.ma new file mode 100644 index 000000000..1623ff030 --- /dev/null +++ b/helm/matita/tests/elim.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/elim". + +inductive stupidtype: Set \def + | Base : stupidtype + | Next : stupidtype \to stupidtype + | Pair : stupidtype \to stupidtype \to stupidtype. + +alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "exists" (instance 0) = "exists". +alias symbol "or" (instance 0) = "logical or". + +theorem serious: + \forall a:stupidtype. + a = Base + \lor + (\exists b:stupidtype.a = Next b) + \lor + (\exists c,d:stupidtype.a = Pair c d). +intros. +elim a. +clear a.left.left. + reflexivity. +clear H.clear H1.clear a.right. + exists.exact e2.exists.exact e1.reflexivity. +clear H.clear a.left.right. + exists.exact e3.reflexivity. +qed. \ No newline at end of file -- 2.39.2