]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/core_notation.moo
New declarative commands (ast, pretty-printing and parsing only):
[helm.git] / helm / software / matita / core_notation.moo
1 notation "hvbox(a break \to b)" 
2   right associative with precedence 20
3 for @{ \forall $_:$a.$b }.
4
5 notation < "hvbox(a break \to b)" 
6   right associative with precedence 20
7 for @{ \Pi $_:$a.$b }.
8
9 notation "hvbox(a break = b)" 
10   non associative with precedence 45
11 for @{ 'eq $a $b }.
12
13 notation "hvbox(a break \leq b)" 
14   non associative with precedence 45
15 for @{ 'leq $a $b }.
16
17 notation "hvbox(a break \geq b)" 
18   non associative with precedence 45
19 for @{ 'geq $a $b }.
20
21 notation "hvbox(a break \lt b)" 
22   non associative with precedence 45
23 for @{ 'lt $a $b }.
24
25 notation "hvbox(a break \gt b)" 
26   non associative with precedence 45
27 for @{ 'gt $a $b }.
28
29 notation "hvbox(a break \neq b)" 
30   non associative with precedence 45
31 for @{ 'neq $a $b }.
32
33 notation "hvbox(a break \nleq b)" 
34   non associative with precedence 45
35 for @{ 'nleq $a $b }.
36
37 notation "hvbox(a break \ngeq b)" 
38   non associative with precedence 45
39 for @{ 'ngeq $a $b }.
40
41 notation "hvbox(a break \nless b)" 
42   non associative with precedence 45
43 for @{ 'nless $a $b }.
44
45 notation "hvbox(a break \ngtr b)" 
46   non associative with precedence 45
47 for @{ 'ngtr $a $b }.
48
49 notation "hvbox(a break \divides b)"
50   non associative with precedence 45
51 for @{ 'divides $a $b }.
52
53 notation "hvbox(a break \ndivides b)"
54   non associative with precedence 45
55 for @{ 'ndivides $a $b }.
56
57 notation "hvbox(a break + b)" 
58   left associative with precedence 50
59 for @{ 'plus $a $b }.
60
61 notation "hvbox(a break - b)" 
62   left associative with precedence 50
63 for @{ 'minus $a $b }.
64
65 notation "hvbox(a break * b)" 
66   left associative with precedence 55
67 for @{ 'times $a $b }.
68
69 notation "hvbox(a break \mod b)" 
70   left associative with precedence 55
71 for @{ 'module $a $b }.
72
73 notation "\frac a b" 
74   non associative with precedence 90
75 for @{ 'divide $a $b }.
76
77 notation "a \over b" 
78   left associative with precedence 55
79 for @{ 'divide $a $b }.
80
81 notation "hvbox(a break / b)" 
82   left associative with precedence 55
83 for @{ 'divide $a $b }.
84
85 notation > "- a" 
86   right associative with precedence 60
87 for @{ 'uminus $a }.
88
89 notation < "- a" 
90   right associative with precedence 75
91 for @{ 'uminus $a }.
92
93 notation "a !"
94   non associative with precedence 80
95 for @{ 'fact $a }.
96
97 notation "(a \sup b)"
98   right associative with precedence 65
99 for @{ 'exp $a $b}.
100
101 notation "\sqrt a" 
102   non associative with precedence 60
103 for @{ 'sqrt $a }.
104
105 notation "hvbox(a break \lor b)" 
106   left associative with precedence 30
107 for @{ 'or $a $b }.
108
109 notation "hvbox(a break \land b)" 
110   left associative with precedence 35
111 for @{ 'and $a $b }.
112
113 notation "hvbox(\lnot a)" 
114   left associative with precedence 40
115 for @{ 'not $a }.