Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extranat.ma

    r744 r961  
    1919    ]
    2020].
     21
     22lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n.
     23#n elim n
     24[ @refl
     25| #m #IH whd in ⊢ (??%?) > IH @refl
     26] qed.
     27
     28lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m.
     29#n #m elim n
     30[ //
     31| #n' #IH whd in ⊢ (??%?) > IH @refl
     32] qed.
     33
     34lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m.
     35#n #m elim m
     36[ //
     37| #m' #IH whd in ⊢ (??%?) > IH @refl
     38] qed.
    2139
    2240lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.
Note: See TracChangeset for help on using the changeset viewer.