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