From 0e10d3bcb924a36596134edfa3d82431c7794e09 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jul 2005 13:44:39 +0000 Subject: [PATCH] added test for change --- helm/matita/tests/change.ma | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 helm/matita/tests/change.ma diff --git a/helm/matita/tests/change.ma b/helm/matita/tests/change.ma new file mode 100644 index 000000000..ea894c28e --- /dev/null +++ b/helm/matita/tests/change.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/change/". +alias num (instance 0) = "natural number". +alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "plus" (instance 0) = "natural plus". +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". + +theorem stupid: + \forall a:nat. + a = 5 \to + (3 + 2) = a. +intros. +change in \vdash (? ? % ?) with 5. +rewrite < H in \vdash (? ? % ?). +reflexivity. +qed. \ No newline at end of file -- 2.39.2