From 50371578cbaffb42e686a2c4389ba2bb52a2c503 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 8 Sep 2007 23:40:19 +0000 Subject: [PATCH] better test for church numerals --- helm/software/matita/tests/coercions.ma | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/helm/software/matita/tests/coercions.ma b/helm/software/matita/tests/coercions.ma index 3d788a813..ca8c4abab 100644 --- a/helm/software/matita/tests/coercions.ma +++ b/helm/software/matita/tests/coercions.ma @@ -107,10 +107,24 @@ definition map: \forall n:nat.\forall l:listn nat n. nat \to nat \def definition church: nat \to nat \to nat \def times. coercion cic:/matita/tests/coercions/church.con 1. +lemma foo0 : ∀n:nat. n n = n * n. +intros; reflexivity; +qed. +lemma foo01 : ∀n:nat. n n n = n * n * n. +intros; reflexivity; +qed. definition mapmult: \forall n:nat.\forall l:listn nat n. nat \to nat \to nat \def \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat. l (m m) o (o o o). + +lemma foo : ∀n:nat. n n n n n n = n * n * n * n * n * n. +intros; reflexivity; +qed. + +axiom f : nat → nat. + +lemma foo1 : ∀n:nat. f n n = f n * n. axiom T0 : Type. axiom T1 : Type. -- 2.39.2