Changeset 712 for src/ASM/Util.ma


Ignore:
Timestamp:
Mar 28, 2011, 5:40:51 PM (9 years ago)
Author:
mulligan
Message:

Changes to get things to typecheck.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r704 r712  
    1 include "arithmetics/nat.ma".
    21include "basics/list.ma".
    32include "basics/types.ma".
     3include "arithmetics/nat.ma".
    44
    55let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
     
    4343definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
    4444
    45 let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝
    46 match l with
    47 [ nil ⇒ r
    48 | cons h t ⇒ revapp T t (h::r)
    49 ].
    50 
    51 definition rev ≝ λT:Type[0].λl. revapp T l [ ].
    52 
    5345lemma eq_rect_Type0_r :
    5446  ∀A: Type[0].
     
    10597        ]
    10698    ].
    107 
     99   
    108100definition ltb ≝
    109101  λm, n: nat.
     
    118110    leb n m.
    119111
     112(* dpm: conflicts with library definitions
    120113interpretation "Nat less than" 'lt m n = (ltb m n).
    121114interpretation "Nat greater than" 'gt m n = (gtb m n).
    122115interpretation "Nat greater than eq" 'geq m n = (geb m n).
     116*)
    123117
    124118let rec division_aux (m: nat) (n : nat) (p: nat) ≝
Note: See TracChangeset for help on using the changeset viewer.