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 (* GENERIC NOTATION *********************************************************)
17 (* Note: this should go to core_notation *)
19 non associative with precedence 90
22 (* Note: this should go to core_notation *)
24 non associative with precedence 90
27 (* Note: this should go to core_notation *)
28 notation "hvbox(a break โบ b)"
29 non associative with precedence 45
32 notation "hvbox( # term 90 i )"
33 non associative with precedence 46
34 for @{ 'VariableReferenceByIndex $i }.
36 notation "hvbox( { term 46 b } # break term 90 i )"
37 non associative with precedence 46
38 for @{ 'VariableReferenceByIndex $b $i }.
40 notation "hvbox( ๐ . term 46 A )"
41 non associative with precedence 46
42 for @{ 'Abstraction $A }.
44 notation "hvbox( { term 46 b } ๐ . break term 46 T)"
45 non associative with precedence 46
46 for @{ 'Abstraction $b $T }.
48 notation "hvbox( @ term 46 C . break term 46 A )"
49 non associative with precedence 46
50 for @{ 'Application $C $A }.
52 notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )"
53 non associative with precedence 46
54 for @{ 'Application $b $V $T }.
56 notation "hvbox( โ [ term 46 d , break term 46 h ] break term 46 M )"
57 non associative with precedence 46
58 for @{ 'Lift $h $d $M }.
60 notation > "hvbox( โ [ term 46 h ] break term 46 M )"
61 non associative with precedence 46
62 for @{ 'Lift $h 0 $M }.
64 notation > "hvbox( โ term 46 M )"
65 non associative with precedence 46
66 for @{ 'Lift 1 0 $M }.
68 (* Note: the notation with "/" does not work *)
69 notation "hvbox( [ term 46 d break โ term 46 N ] break term 46 M )"
70 non associative with precedence 46
71 for @{ 'DSubst $N $d $M }.
73 notation > "hvbox( [ โ term 46 N ] break term 46 M )"
74 non associative with precedence 46
75 for @{ 'DSubst $N 0 $M }.
77 (* Note: we do not use โ since it is reserved by CIC *)
78 notation "hvbox( M break โฆ term 46 N )"
79 non associative with precedence 45
80 for @{ 'SeqRed $M $N }.
82 notation "hvbox( M break โฆ [ term 46 p ] break term 46 N )"
83 non associative with precedence 45
84 for @{ 'SeqRed $M $p $N }.
86 notation "hvbox( M break โฆ* term 46 N )"
87 non associative with precedence 45
88 for @{ 'SeqRedStar $M $N }.
90 notation "hvbox( M break โฆ* [ term 46 s ] break term 46 N )"
91 non associative with precedence 45
92 for @{ 'SeqRedStar $M $s $N }.
94 notation "hvbox( M break โค term 46 N )"
95 non associative with precedence 45
96 for @{ 'ParRed $M $N }.
98 notation "hvbox( M break โค* term 46 N )"
99 non associative with precedence 45
100 for @{ 'ParRedStar $M $N }.