From b6afef7e73324824025a6d7f313129d55b72cfc6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Jul 2009 16:30:17 +0000 Subject: [PATCH] claudio, please have a look at this --- helm/software/matita/tests/ng_coercions.ma | 34 +++++++++++++++------- 1 file changed, 23 insertions(+), 11 deletions(-) diff --git a/helm/software/matita/tests/ng_coercions.ma b/helm/software/matita/tests/ng_coercions.ma index 1a1686267..308697d3c 100644 --- a/helm/software/matita/tests/ng_coercions.ma +++ b/helm/software/matita/tests/ng_coercions.ma @@ -12,19 +12,31 @@ (* *) (**************************************************************************) -axiom A : Type. -axiom B : Type. -axiom C : Type. +include "ng_pts.ma". -axiom f : A → B. -axiom g : B → C. +ninductive list (A : Type) : Type ≝ + | nil : list A + | cons : A → list A → list A. -(* nlemma xxx : ∀P:C → Prop. ∀x:A. P x. *) +naxiom T : Type. +naxiom S : Type. +naxiom c : list T → list S. -coercion f. coercion g. +ncoercion foo : ∀_l:list T. list S ≝ c + on _l : list T + to list ?. + +naxiom P : list S → Prop. + +ndefinition t1 ≝ ∀x:list T.P x → ?. ##[ napply Prop; ##] nqed. + +ncoercion bar : ∀_l:list T. S → S ≝ λ_.λx.x + on _l : list T + to Π_.?. + +naxiom Q : (S → S) → Prop. -axiom T : Type. +ndefinition t2 ≝ ∀x:list T.Q x → ?. ##[ napply Prop; ##] nqed. -axiom h : A → T. coercion h. - -nlemma xxx : ∀P:C → Prop. ∀x:A. P x. \ No newline at end of file + + \ No newline at end of file -- 2.39.2