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 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "common/pts.ma".
27 Notation for hint declaration
28 ==============================
30 The idea is to write a context, with abstraction first, then
31 recursive calls (let-in) and finally the two equivalent terms.
32 The context can be empty. Note the ; to begin the second part of
33 the context (necessary even if the first part is empty).
35 unification hint PREC \coloneq
37 ; ID \equest T, ..., ID \equest T
40 With unidoce and some ASCII art it looks like the following:
42 unification hint PREC ≔ ID : TY, ..., ID : TY;
44 (*---------------------*) ⊢
49 (* it seems unbelivable, but it works! *)
50 notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 90 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py"
55 @{ 'hint_decl $Px $Py }
56 rec acc1 @{ let ( ${ident U} : ?) ≝ $V in $acc1} } }
57 @{ 'hint_decl $Px $Py }
61 ${ fold right @{ $acc } rec acc2
62 @{ ∀${ident x}:${ default @{ $T } @{ ? } }.$acc2 } }
66 ndefinition hint_declaration_Type0 ≝ λA:Type[0].λa,b:A.Prop.
67 ndefinition hint_declaration_Type1 ≝ λA:Type[1].λa,b:A.Prop.
68 ndefinition hint_declaration_Type2 ≝ λa,b:Type[2].Prop.
69 ndefinition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.Prop.
70 ndefinition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.Prop.
71 ndefinition hint_declaration_CProp2 ≝ λa,b:CProp[2].Prop.
73 interpretation "hint_decl_Type2" 'hint_decl a b = (hint_declaration_Type2 a b).
74 interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).
75 interpretation "hint_decl_Type1" 'hint_decl a b = (hint_declaration_Type1 ? a b).
76 interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a b).
77 interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b).
78 interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b).