Changeset 260 for Deliverables/D4.1/Matita/Nat.ma
 Timestamp:
 Nov 23, 2010, 2:30:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Nat.ma
r247 r260 24 24 nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝ 25 25 match m with 26 [ Z ⇒ True26 [ Z ⇒ true 27 27  S o ⇒ 28 28 match n with 29 [ Z ⇒ False29 [ Z ⇒ false 30 30  S p ⇒ less_than_or_equal_b o p 31 31 ] … … 125 125 nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝ 126 126 match n ≤ p with 127 [ True ⇒ Z128  False ⇒127 [ true ⇒ Z 128  false ⇒ 129 129 match m with 130 130 [ Z ⇒ Z … … 148 148 nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝ 149 149 match n ≤ p with 150 [ True ⇒ n151  False ⇒150 [ true ⇒ n 151  false ⇒ 152 152 match m with 153 153 [ Z ⇒ n
Note: See TracChangeset
for help on using the changeset viewer.