From 8a8cb7db0c80d9945969960e69f440ca326e2b92 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 29 Aug 2006 11:00:22 +0000 Subject: [PATCH] test file with some bugs --- helm/software/matita/contribs/prova.ma | 27 ++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 helm/software/matita/contribs/prova.ma diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma new file mode 100644 index 000000000..407db9b66 --- /dev/null +++ b/helm/software/matita/contribs/prova.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/test/". + +include "nat/nat.ma". + +theorem pippo: \forall (P,Q,R:nat \to Prop). + \forall x,y. x=y \to P x \to Q x \to R x. + intros. + try rewrite > P in Q. +(* +theorem pippo2: \forall (P,Q,R:nat \to Prop). + \forall x,y. x=y \to P x \to Q x \to R x. + intros. rewrite > H in y. +*) -- 2.39.2