helm/software/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