1 notation "hvbox(a break \to b)"
2 right associative with precedence 20
3 for @{ \forall $_:$a.$b }.
5 notation < "hvbox(a break \to b)"
6 right associative with precedence 20
9 notation "hvbox(a break = b)"
10 non associative with precedence 45
13 notation "hvbox(a break \leq b)"
14 non associative with precedence 45
17 notation "hvbox(a break \geq b)"
18 non associative with precedence 45
21 notation "hvbox(a break \lt b)"
22 non associative with precedence 45
25 notation "hvbox(a break \gt b)"
26 non associative with precedence 45
29 notation "hvbox(a break \neq b)"
30 non associative with precedence 45
33 notation "hvbox(a break + b)"
34 left associative with precedence 50
37 notation "hvbox(a break - b)"
38 left associative with precedence 50
39 for @{ 'minus $a $b }.
41 notation "hvbox(a break * b)"
42 left associative with precedence 55
43 for @{ 'times $a $b }.
45 notation "hvbox(a break / b)"
46 left associative with precedence 55
47 for @{ 'divide $a $b }.
50 non associative with precedence 90
51 for @{ 'divide $a $b }.
54 left associative with precedence 55
55 for @{ 'divide $a $b }.
58 non associative with precedence 60
62 non associative with precedence 60
65 notation "hvbox(a break \lor b)"
66 left associative with precedence 30
69 notation "hvbox(a break \land b)"
70 left associative with precedence 35
73 notation "hvbox(\lnot a)"
74 left associative with precedence 40
77 (* aritmetic operators *)
79 interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
80 interpretation "Coq's real plus" 'plus x y = (cic:/Coq/Reals/Rdefinitions/Rplus.con x y).
81 interpretation "Coq's binary integer plus" 'plus x y = (cic:/Coq/ZArith/BinInt/Zplus.con x y).
82 interpretation "Coq's binary positive plus" 'plus x y = (cic:/Coq/NArith/BinPos/Pplus.con x y).
83 interpretation "Coq's natural minus" 'minus x y = (cic:/Coq/Init/Peano/minus.con x y).
84 interpretation "Coq's real minus" 'minus x y = (cic:/Coq/Reals/Rdefinitions/Rminus.con x y).
85 interpretation "Coq's binary integer minus" 'minus x y = (cic:/Coq/ZArith/BinInt/Zminus.con x y).
86 interpretation "Coq's binary positive minus" 'minus x y = (cic:/Coq/NArith/BinPos/Pminus.con x y).
87 interpretation "Coq's natural times" 'times x y = (cic:/Coq/Init/Peano/mult.con x y).
88 interpretation "Coq's real times" 'times x y = (cic:/Coq/Reals/Rdefinitions/Rmult.con x y).
89 interpretation "Coq's binary positive times" 'times x y = (cic:/Coq/NArith/BinPos/Pmult.con x y).
90 interpretation "Coq's binary integer times" 'times x y = (cic:/Coq/ZArith/BinInt/Zmult.con x y).
91 interpretation "Coq's real power" 'power x y = (cic:/Coq/Reals/Rfunctions/pow.con x y).
92 interpretation "Coq's integer power" 'power x y = (cic:/Coq/ZArith/Zpower/Zpower.con x y).
93 interpretation "Coq's real divide" 'divide x y = (cic:/Coq/Reals/Rdefinitions/Rdiv.con x y).
94 interpretation "Coq's real unary minus" 'uminus x = (cic:/Coq/Reals/Rdefinitions/Ropp.con x).
95 interpretation "Coq's binary integer negative sign" 'uminus x = (cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/3) x).
96 interpretation "Coq's binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/BinInt/Zopp.con x).
98 (* logical operators *)
100 interpretation "Coq's logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y).
101 interpretation "Coq's logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y).
102 interpretation "Coq's logical not" 'not x = (cic:/Coq/Init/Logic/not.con x).
103 interpretation "Coq's exists" 'exists x y = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) x y).
105 (* relational operators *)
107 interpretation "Coq's natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y).
108 interpretation "Coq's real 'less or equal to'" 'leq x y = (cic:/Coq/Reals/Rdefinitions/Rle.con x y).
109 interpretation "Coq's natural 'greater or equal to'" 'geq x y = (cic:/Coq/Init/Peano/ge.con x y).
110 interpretation "Coq's real 'greater or equal to'" 'geq x y = (cic:/Coq/Reals/Rdefinitions/Rge.con x y).
111 interpretation "Coq's natural 'less than'" 'lt x y = (cic:/Coq/Init/Peano/lt.con x y).
112 interpretation "Coq's real 'less than'" 'lt x y = (cic:/Coq/Reals/Rdefinitions/Rlt.con x y).
113 interpretation "Coq's natural 'greater than'" 'gt x y = (cic:/Coq/Init/Peano/gt.con x y).
114 interpretation "Coq's real 'greater than'" 'gt x y = (cic:/Coq/Reals/Rdefinitions/Rgt.con x y).
116 interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y).
117 interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)).