Changeset 275 for Deliverables/D4.1/Matita/Nat.ma
- Timestamp:
- Nov 24, 2010, 3:40:37 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/Nat.ma
r265 r275 43 43 n ≤ m. 44 44 45 ndefinition greater_than_or_equal_b ≝45 ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝ 46 46 λm, n: Nat. 47 47 n ≤ m. … … 190 190 interpretation "Nat exponential" 'exponential n m = (exponential n m). 191 191 192 nlet rec decidable_equality (m: Nat) (n: Nat) on m: Bool ≝ 193 match m with 194 [ Z ⇒ 195 match n with 196 [ Z ⇒ true 197 | _ ⇒ false 198 ] 199 | S o ⇒ 200 match n with 201 [ S p ⇒ decidable_equality o p 202 | _ ⇒ false 203 ] 204 ]. 205 192 206 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 193 207 (* Greatest common divisor and least common multiple. *)
Note: See TracChangeset
for help on using the changeset viewer.