Changeset 712 for src/ASM/Util.ma
 Timestamp:
 Mar 28, 2011, 5:40:51 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r704 r712 1 include "arithmetics/nat.ma".2 1 include "basics/list.ma". 3 2 include "basics/types.ma". 3 include "arithmetics/nat.ma". 4 4 5 5 let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝ … … 43 43 definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. 44 44 45 let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝46 match l with47 [ nil ⇒ r48  cons h t ⇒ revapp T t (h::r)49 ].50 51 definition rev ≝ λT:Type[0].λl. revapp T l [ ].52 53 45 lemma eq_rect_Type0_r : 54 46 ∀A: Type[0]. … … 105 97 ] 106 98 ]. 107 99 108 100 definition ltb ≝ 109 101 λm, n: nat. … … 118 110 leb n m. 119 111 112 (* dpm: conflicts with library definitions 120 113 interpretation "Nat less than" 'lt m n = (ltb m n). 121 114 interpretation "Nat greater than" 'gt m n = (gtb m n). 122 115 interpretation "Nat greater than eq" 'geq m n = (geb m n). 116 *) 123 117 124 118 let rec division_aux (m: nat) (n : nat) (p: nat) ≝
Note: See TracChangeset
for help on using the changeset viewer.