Changeset 237 for Deliverables/D4.1/Matita/Nat.ma
 Timestamp:
 Nov 12, 2010, 4:51:45 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Nat.ma
r236 r237 34 34 ]. 35 35 36 notation " n break ≤ m"36 notation "hvbox(n break ≤ m)" 37 37 non associative with precedence 47 38 38 for @{ 'less_than_or_equal $n $m }. … … 49 49 n ≤ m. 50 50 51 notation " n break ≥ m"51 notation "hvbox(n break ≥ m)" 52 52 non associative with precedence 47 53 53 for @{ 'greater_than_or_equal $n $m }. … … 62 62 m ≤ n ∧ ¬(m = n). 63 63 64 notation " n break < m"64 notation "hvbox(n break < m)" 65 65 non associative with precedence 47 66 66 for @{ 'less_than $n $m }. … … 72 72 n < m. 73 73 74 notation " n break > m"74 notation "hvbox(n break > m)" 75 75 non associative with precedence 47 76 76 for @{ 'greater_than $n $m }. … … 87 87 ]. 88 88 89 notation " n break + m"89 notation "hvbox(n break + m)" 90 90 right associative with precedence 52 91 91 for @{ 'plus $n $m }. … … 103 103 ]. 104 104 105 notation " n break  m"105 notation "hvbox(n break  m)" 106 106 right associative with precedence 47 107 107 for @{ 'minus $n $m }. … … 119 119 ]. 120 120 121 notation " n break * m"121 notation "hvbox(n break * m)" 122 122 right associative with precedence 47 123 123 for @{ 'multiplication $n $m }. … … 142 142 ]. 143 143 144 notation " n break ÷ m"144 notation "hvbox(n break ÷ m)" 145 145 right associative with precedence 47 146 146 for @{ 'division $n $m }. … … 165 165 ]. 166 166 167 notation " n break % m"167 notation "hvbox(n break % m)" 168 168 right associative with precedence 47 169 169 for @{ 'modulus $n $m }. 170 170 171 171 interpretation "Nat modulus" 'modulus m n = (modulus m n). 172 173 ndefinition divide_with_remainder ≝ 174 λm, n: Nat. 175 mk_Cartesian Nat Nat (m ÷ n) (modulus m n). 176 177 (* ===================================== *) 178 (* Exponentials, and square roots. *) 179 (* ===================================== *) 180 181 nlet rec exponential (m: Nat) (n: Nat) on n ≝ 182 match n with 183 [ Z ⇒ S (Z) 184  S o ⇒ m * exponential m o 185 ]. 186 187 notation "hvbox(n ^ m)" 188 left associative with precedence 52 189 for @{ 'exponential $n $m }. 190 191 interpretation "Nat exponential" 'exponential n m = (exponential n m). 172 192 173 193 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.