Changeset 2773 for extracted/lists.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/lists.ml

    r2743 r2773  
    2727open Util
    2828
    29 (** val all0 : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
    30 let rec all0 p = function
     29(** val all : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
     30let rec all p = function
    3131| List.Nil -> Bool.True
    32 | List.Cons (h, t) -> Bool.andb (p h) (all0 p t)
    33 
    34 type ('x, 'x0) all2 = __
     32| List.Cons (h, t) -> Bool.andb (p h) (all p t)
    3533
    3634(** val map_All : ('a1 -> __ -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
     
    3836  (match l with
    3937   | List.Nil -> (fun _ -> List.Nil)
    40    | List.Cons (hd0, tl) -> (fun _ -> List.Cons ((f hd0 __), (map_All f tl))))
     38   | List.Cons (hd, tl) -> (fun _ -> List.Cons ((f hd __), (map_All f tl))))
    4139    __
    4240
     
    4745open Option
    4846
    49 (** val append0 : 'a1 List.list List.aop **)
    50 let append0 =
     47(** val append : 'a1 List.list List.aop **)
     48let append =
    5149  List.append
    5250
    53 (** val list0 : Monad.monadProps **)
    54 let list0 =
     51(** val list : Monad.monadProps **)
     52let list =
    5553  Monad.makeMonadProps (fun _ x -> List.Cons (x, List.Nil)) (fun _ _ l f ->
    5654    List.foldr (fun x -> List.append (f x)) List.Nil l)
Note: See TracChangeset for help on using the changeset viewer.