1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 Notation for hint declaration
18 ==============================
20 The idea is to write a context, with abstraction first, then
21 recursive calls (let-in) and finally the two equivalent terms.
22 The context can be empty. Note the ; to begin the second part of
23 the context (necessary even if the first part is empty).
25 unification hint PREC \coloneq
27 ; ID \equest T, ..., ID \equest T
30 With unidoce and some ASCII art it looks like the following:
32 unification hint PREC ≔ ID : TY, ..., ID : TY;
34 (*---------------------*) ⊢
39 (* it seems unbelivable, but it works! *)
40 notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 19 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py"
45 @{ 'hint_decl $Px $Py }
46 rec acc1 @{ let ( ${ident U} : ?) ≝ $V in $acc1} } }
47 @{ 'hint_decl $Px $Py }
51 ${ fold right @{ $acc } rec acc2
52 @{ ∀${ident x}:${ default @{ $T } @{ ? } }.$acc2 } }
56 include "logic/pts.ma".
58 ndefinition hint_declaration_Type0 ≝ λA:Type[0] .λa,b:A.Prop.
59 ndefinition hint_declaration_Type1 ≝ λA:Type[1].λa,b:A.Prop.
60 ndefinition hint_declaration_Type2 ≝ λa,b:Type[2].Prop.
61 ndefinition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.Prop.
62 ndefinition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.Prop.
63 ndefinition hint_declaration_CProp2 ≝ λa,b:CProp[2].Prop.
65 interpretation "hint_decl_Type2" 'hint_decl a b = (hint_declaration_Type2 a b).
66 interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).
67 interpretation "hint_decl_Type1" 'hint_decl a b = (hint_declaration_Type1 ? a b).
68 interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a b).
69 interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b).
70 interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b).
72 (* Non uniform coercions support *)
73 nrecord lock2 (S : Type[2]) (s : S) : Type[3] ≝ {
78 nrecord lock1 (S : Type[1]) (s : S) : Type[2] ≝ {
83 ncoercion lift1 : ∀S:Type[1].∀s:S.∀l:lock1 S s. force1 S s l ≝ lift1
84 on s : ? to force1 ???.
86 ncoercion lift2 : ∀S:Type[2].∀s:S.∀l:lock2 S s. force2 S s l ≝ lift2
87 on s : ? to force2 ???.
89 (* Example of a non uniform coercion declaration
97 unification hint 0 ≔ R : setoid;
99 lock ≟ mk_lock1 Type[0] MR setoid R
100 (* ---------------------------------------- *) ⊢
101 setoid ≡ force1 ? MR lock.