]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/tests/ng_coercion_and_hints.ma
update in basic_2
[helm.git] / matitaB / matita / tests / ng_coercion_and_hints.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ng_pts.ma".
16 ndefinition hint_declaration_Type0  ≝  λA:Type[0] .λa,b:A.a.
17 ndefinition hint_declaration_Type1  ≝  λA:Type[1].λa,b:A.a.
18 ndefinition hint_declaration_Type2  ≝  λa,b:Type[1].a.
19 ndefinition hint_declaration_CProp0 ≝  λA:CProp[0].λa,b:A.a.
20 ndefinition hint_declaration_CProp1 ≝  λA:CProp[1].λa,b:A.a.
21 ndefinition hint_declaration_CProp2 ≝  λa,b:CProp[1].a.
22   
23 notation > "≔ (list0 (ident x : T )sep ,) ⊢ term 19 Px ≡ term 19 Py"
24   with precedence 90
25   for @{ ${ fold right @{'hint_decl $Px $Py} rec acc @{ ∀${ident x}:$T.$acc } } }.      
26
27 interpretation "hint_decl_Type2"  'hint_decl a b = (hint_declaration_Type2 a b).
28 interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).
29 interpretation "hint_decl_Type1"  'hint_decl a b = (hint_declaration_Type1 ? a b).
30 interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a b).
31 interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b).
32 interpretation "hint_decl_Type0"  'hint_decl a b = (hint_declaration_Type0 ? a b).
33
34 naxiom A : Type[0].
35 naxiom B : Type[0].
36
37 ndefinition C ≝ B.
38 ndefinition D ≝ A.
39
40 naxiom f : B → A.
41
42 ncoercion pippo : ∀a:B. A ≝ f on _a : B to A.
43
44 alias symbol "hint_decl" = "hint_decl_Type1".
45 unification hint 0 ≔ ⊢ C ≡ B.
46 unification hint 0 ≔ ⊢ A ≡ D.
47
48 naxiom pippo : D → Prop.
49
50 nlemma foo : ∀c:C. pippo c. 
51
52