From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Jul 2009 16:30:17 +0000 (+0000)
Subject: claudio, please have a look at this
X-Git-Tag: make_still_working~3710
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b6afef7e73324824025a6d7f313129d55b72cfc6;p=helm.git

claudio, please have a look at this
---

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