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.