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 *)
18 notation "hvbox(a break โบ b)"
19 non associative with precedence 45
22 notation "hvbox( # term 90 i )"
23 non associative with precedence 46
24 for @{ 'VariableReferenceByIndex $i }.
26 notation "hvbox( { term 46 b } # break term 90 i )"
27 non associative with precedence 46
28 for @{ 'VariableReferenceByIndex $b $i }.
30 notation "hvbox( ๐ . term 46 A )"
31 non associative with precedence 46
32 for @{ 'Abstraction $A }.
34 notation "hvbox( { term 46 b } ๐ . break term 46 T)"
35 non associative with precedence 46
36 for @{ 'Abstraction $b $T }.
38 notation "hvbox( @ term 46 C . break term 46 A )"
39 non associative with precedence 46
40 for @{ 'Application $C $A }.
42 notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )"
43 non associative with precedence 46
44 for @{ 'Application $b $V $T }.
46 notation "hvbox( โ [ term 46 d , break term 46 h ] break term 46 M )"
47 non associative with precedence 46
48 for @{ 'Lift $h $d $M }.
50 notation > "hvbox( โ [ term 46 h ] break term 46 M )"
51 non associative with precedence 46
52 for @{ 'Lift $h 0 $M }.
54 notation > "hvbox( โ term 46 M )"
55 non associative with precedence 46
56 for @{ 'Lift 1 0 $M }.
58 (* Note: the notation with "/" does not work *)
59 notation "hvbox( [ term 46 d break โ term 46 N ] break term 46 M )"
60 non associative with precedence 46
61 for @{ 'DSubst $N $d $M }.
63 notation > "hvbox( [ โ term 46 N ] break term 46 M )"
64 non associative with precedence 46
65 for @{ 'DSubst $N 0 $M }.
67 (* Note: we do not use โ since it is reserved by CIC *)
68 notation "hvbox( M break โฆ term 46 N )"
69 non associative with precedence 45
70 for @{ 'SeqRed $M $N }.
72 notation "hvbox( M break โฆ [ term 46 p ] break term 46 N )"
73 non associative with precedence 45
74 for @{ 'SeqRed $M $p $N }.
76 notation "hvbox( M break โฆ* term 46 N )"
77 non associative with precedence 45
78 for @{ 'SeqRedStar $M $N }.
80 notation "hvbox( M break โฆ* [ term 46 s ] break term 46 N )"
81 non associative with precedence 45
82 for @{ 'SeqRedStar $M $s $N }.
84 notation "hvbox( M break โค term 46 N )"
85 non associative with precedence 45
86 for @{ 'ParRed $M $N }.
88 notation "hvbox( M break โค* term 46 N )"
89 non associative with precedence 45
90 for @{ 'ParRedStar $M $N }.