TFL/tfl.sml
changeset 3712 242546f35f8e
parent 3459 112cbb8301dc
child 3768 67f4ac759100
equal deleted inserted replaced
3711:2f86b403d975 3712:242546f35f8e
    17 val concl = #2 o R.dest_thm;
    17 val concl = #2 o R.dest_thm;
    18 val hyp = #1 o R.dest_thm;
    18 val hyp = #1 o R.dest_thm;
    19 
    19 
    20 val list_mk_type = U.end_itlist (curry(op -->));
    20 val list_mk_type = U.end_itlist (curry(op -->));
    21 
    21 
    22 fun gtake f =
    22 fun enumerate l = 
    23   let fun grab(0,rst) = ([],rst)
    23      rev(#1(foldl (fn ((alist,i), x) => ((x,i)::alist, i+1)) (([],0), l)));
    24         | grab(n, x::rst) = 
       
    25              let val (taken,left) = grab(n-1,rst)
       
    26              in (f x::taken, left) end
       
    27   in grab
       
    28   end;
       
    29 
       
    30 fun enumerate L = 
       
    31  rev(#1(U.rev_itlist (fn x => fn (alist,i) => ((x,i)::alist, i+1)) L ([],0)));
       
    32 
    24 
    33 fun stringize [] = ""
    25 fun stringize [] = ""
    34   | stringize [i] = Int.toString i
    26   | stringize [i] = Int.toString i
    35   | stringize (h::t) = (Int.toString h^", "^stringize t);
    27   | stringize (h::t) = (Int.toString h^", "^stringize t);
    36 
    28