Changeset 231 for Deliverables/D4.1/Matita/Nat.ma
- Timestamp:
- Nov 11, 2010, 12:27:04 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/Nat.ma
r230 r231 50 50 interpretation "Nat multiplication" 'times n m = (multiplication n m). 51 51 52 nlet rec less_than_or_equal (n: Nat) (m: Nat) ≝ 53 match n with 54 [ Z ⇒ True 55 | S o ⇒ 56 match m with 57 [ Z ⇒ False 58 | S p ⇒ less_than_or_equal o p 59 ] 60 ]. 61 62 notation "n break ≤ m" 63 non associative with precedence 47 64 for @{ 'less_than_or_equal $n $m }. 65 66 interpretation "Nat less than or equal" 'less_than_or_equal n m = (less_than_or_equal n m). 67 52 68 nlemma plus_zero: 53 69 ∀n: Nat.
Note: See TracChangeset
for help on using the changeset viewer.