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 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
17 (* Grammar ******************************************************************)
20 non associative with precedence 90
23 notation "hvbox( ⋆ term 90 k )"
24 non associative with precedence 90
27 notation "hvbox( 𝕚 { I } break (term 90 T1) . break (term 90 T) )"
28 non associative with precedence 90
29 for @{ 'SItem $I $T1 $T }.
31 notation "hvbox( 𝕓 { I } break (term 90 T1) . break (term 90 T) )"
32 non associative with precedence 90
33 for @{ 'SBind $I $T1 $T }.
35 notation "hvbox( 𝕗 { I } break (term 90 T1) . break (term 90 T) )"
36 non associative with precedence 90
37 for @{ 'SFlat $I $T1 $T }.
39 notation "hvbox( T . break 𝕓 { I } break (term 90 T1) )"
40 non associative with precedence 89
41 for @{ 'DBind $T $I $T1 }.
43 notation "hvbox( | L | )"
44 non associative with precedence 70
47 notation "hvbox( # term 90 x )"
48 non associative with precedence 90
51 notation "hvbox( # [ x , break y ] )"
52 non associative with precedence 90
53 for @{ 'Weight $x $y }.
55 (* Substitution *************************************************************)
57 notation "hvbox( T1 break [ d , break e ] ≈ break T2 )"
58 non associative with precedence 45
59 for @{ 'Eq $T1 $d $e $T2 }.
61 notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )"
62 non associative with precedence 45
63 for @{ 'RLift $T1 $d $e $T2 }.
65 notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )"
66 non associative with precedence 45
67 for @{ 'RDrop $L1 $d $e $L2 }.
69 notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫ break T2 )"
70 non associative with precedence 45
71 for @{ 'PSubst $L $T1 $d $e $T2 }.
73 (* Reduction ****************************************************************)
75 notation "hvbox( T1 ⇒ break T2 )"
76 non associative with precedence 45
77 for @{ 'PRed $T1 $T2 }.
79 notation "hvbox( L ⊢ break (term 90 T1) ⇒ break T2 )"
80 non associative with precedence 45
81 for @{ 'PRed $L $T1 $T2 }.