Skip to main content

🍃 List.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Either.
Require Proto_alpha.Environment.Error_monad.
Require Proto_alpha.Environment.Pervasives.
Require Proto_alpha.Environment.Seq.
Import Error_monad.Notations.
Import Pervasives.Notations.

Definition t (a : Set) : Set := list a.

Definition nil : {a : Set}, list a :=
  fun _
  [].

Definition nil_e : {a trace : Set}, Pervasives.result (list a) trace :=
  fun _ _
  return? [].

Definition nil_s : {a : Set}, list a :=
  fun _
  [].

Definition nil_es : {a trace : Set},
  Pervasives.result (list a) trace :=
  fun _ _
  return? [].

Parameter cons_value : {a : Set}, a list a list a.

Definition hd : {a : Set}, list a option a :=
  fun _ l
    match l with
    | []None
    | x :: _Some x
    end.

Definition tl : {a : Set}, list a option (list a) :=
  fun _ l
    match l with
    | []None
    | _x :: mSome m
    end.

Fixpoint nth_z {a : Set} (l : list a) (i : Z.t) {struct l} : option a :=
  match l, i with
  | [], _None
  | x :: _, 0 ⇒ Some x
  | _ :: l, _nth_z l (i - 1)
  end.

Definition nth : {a : Set}, list a int option a :=
  @nth_z.

Definition nth_opt : {a : Set}, list a int option a :=
  @nth_z.

Definition last : {a : Set}, a list a a :=
  fun _ x l
  List.last l x.

Fixpoint last_opt {a : Set} (l: list a) : option a :=
  match l with
  | []None
  | [z]Some z
  | x :: tl ⇒ (last_opt tl)
  end.

Definition find : {a : Set}, (a bool) list a option a :=
  fun a
  List.find (A := a).

Definition find_opt : {a : Set}, (a bool) list a option a :=
  fun _
  find.

Parameter find_map : {a b : Set},
  (a option b) list a option b.

Fixpoint mem {a : Set} (eq_dec : a a bool) (v : a) (l : list a) : bool :=
  match l with
  | []false
  | x :: leq_dec v x || mem eq_dec v l
  end.

Fixpoint assoc {a b : Set}
  (eq : a a bool)
  (k : a)
  (l : list (a × b))
  : option b :=
  match l with
  | []None
  | (h, x) :: tlif eq k h then Some x else assoc eq k tl
  end.

Definition assoc_opt : {a b : Set},
  (a a bool) a list (a × b) option b :=
  fun _ _assoc.

Parameter assq : {a b : Set}, a list (a × b) option b.

Parameter assq_opt : {a b : Set}, a list (a × b) option b.

Fixpoint mem_assoc {a b : Set}
  (eq : a a bool)
  (k : a)
  (l : list (a × b))
  : bool :=
  match l with
  | []false
  | (h, x) :: tleq k h || mem_assoc eq k tl
  end.

Parameter mem_assq : {a b : Set}, a list (a × b) bool.

Fixpoint remove_assoc {a b : Set}
  (eq : a a bool)
  (k : a)
  (l : list (a × b))
  : list (a × b) :=
  match l with
  | [][]
  | (h, x) :: tl
    if eq k h then
      tl
    else
      (h, x) :: remove_assoc eq k tl
  end.

Parameter remove_assq : {a b : Set}, a list (a × b) list (a × b).

Fixpoint nat_init {a trace : Set} (er : trace) (n : nat) (ff : nat a)
  : list a :=
  match n with
  | 0%nat[]
  | S kff 0%nat :: nat_init er k (fun vff (S v))
  end.

Definition init_value {a trace : Set}
  (er : trace) (n : int) (ff : int a)
  : Pervasives.result (list a) trace :=
  match n with
  | Zneg _Pervasives.Error er
  | Z0Pervasives.Ok []
  | Zpos x
    Pervasives.Ok (nat_init er (Z.to_nat n) (fun xff (Z.of_nat x)))
  end.

Fixpoint length {a : Set} (l : list a) : int :=
  match l with
  | [] ⇒ 0
  | _ :: l(length l) +i 1
  end.

Definition rev {a : Set} (l : list a) : list a :=
  Lists.List.rev' l.

Definition concat : {a : Set}, list (list a) list a :=
  fun _
  List.concat.

Definition append : {a : Set}, list a list a list a :=
  fun _
  List.append.

Definition rev_append : {a : Set}, list a list a list a :=
  fun _
  List.rev_append.

Definition flatten : {a : Set}, list (list a) list a :=
  fun _
  List.concat.

Fixpoint combine_aux {a b : Set}
  (list1 : list a)
  (list2 :list b)
  (partial : list (a × b))
  : option (list (a × b)) :=
  match list1, list2 with
  | [], _ :: _ | _ :: _, []None
  | [], []Some partial
  | h1 :: tl1 , h2 :: tl2combine_aux tl1 tl2 ((h1, h2) :: partial)
  end.

Definition combine {a b trace : Set} (er : trace)
  (l1 : list a) (l2 : list b)
  : Pervasives.result (list (a × b)) trace :=
  match combine_aux l1 l2 [] with
  | Some xPervasives.Ok x
  | NonePervasives.Error er
  end.

Parameter rev_combine : {a b trace : Set},
  trace list a list b Pervasives.result (list (a × b)) trace.

Definition split : {a b : Set}, list (a × b) list a × list b :=
  fun _ _
  List.split.

Parameter iter2 : {a b trace : Set},
  trace (a b unit) list a list b
  Pervasives.result unit trace.

Parameter map2 : {a b c trace : Set},
  trace (a b c) list a list b
  Pervasives.result (list c) trace.

Parameter rev_map2 : {a b c trace : Set},
  trace (a b c) list a list b
  Pervasives.result (list c) trace.

Parameter fold_left2 : {a b c trace : Set},
  trace (a b c a) a list b list c
  Pervasives.result a trace.

Parameter fold_right2 : {a b c trace : Set},
  trace (a b c c) list a list b c
  Pervasives.result c trace.

Parameter for_all2 : {a b trace : Set},
  trace (a b bool) list a list b
  Pervasives.result bool trace.

Parameter _exists2 : {a b trace : Set},
  trace (a b bool) list a list b
  Pervasives.result bool trace.

Parameter init_e : {a trace : Set},
  trace int (int Pervasives.result a trace)
  Pervasives.result (list a) trace.

Parameter init_s : {a trace : Set},
  trace int (int a) Pervasives.result (list a) trace.

Parameter init_es : {a trace : Set},
  trace int (int Pervasives.result a trace)
  Pervasives.result (list a) trace.

Parameter init_p : {a trace : Set},
  trace int (int a) Pervasives.result (list a) trace.

Parameter find_e : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result (option a) trace.

Parameter find_s : {a : Set},
  (a bool) list a option a.

Parameter find_es : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result (option a) trace.

Parameter find_map_e : {a b trace : Set},
  (a Pervasives.result (option b) trace) list a
  Pervasives.result (option b) trace.

Parameter find_map_s : {a b : Set},
  (a option b) list a option b.

Parameter find_map_es : {a b trace : Set},
  (a Pervasives.result (option b) trace) list a
  Pervasives.result (option b) trace.

Definition filter : {a : Set}, (a bool) list a list a :=
  fun _
  List.filter.

Parameter filteri : {a : Set}, (int a bool) list a list a.

Parameter find_all : {a : Set}, (a bool) list a list a.

Parameter rev_filter : {a : Set}, (a bool) list a list a.

Parameter rev_filteri : {a : Set},
  (int a bool) list a list a.

Parameter rev_filter_some : {a : Set}, list (option a) list a.

Parameter filter_some : {a : Set}, list (option a) list a.

Parameter rev_filter_ok : {a b : Set},
  list (Pervasives.result a b) list a.

Parameter filter_ok : {a b : Set},
  list (Pervasives.result a b) list a.

Parameter rev_filter_error : {a b : Set},
  list (Pervasives.result a b) list b.

Parameter filter_error : {a b : Set},
  list (Pervasives.result a b) list b.

Parameter rev_filter_left : {a b : Set}, list (Either.t a b) list a.

Parameter filter_left : {a b : Set}, list (Either.t a b) list a.

Parameter rev_filter_right : {a b : Set},
  list (Either.t a b) list b.

Parameter filter_right : {a b : Set}, list (Either.t a b) list b.

Parameter rev_filter_e : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result (list a) trace.

Fixpoint filter_e {a trace : Set}
  (f : a Pervasives.result bool trace) (l : list a)
  : Pervasives.result (list a) trace :=
  match l with
  | []return? []
  | x :: l
    let? b := f x in
    let? l := filter_e f l in
    if b then
      return? (x :: l)
    else
      return? l
  end.

Parameter rev_filter_s : {a : Set},
  (a bool) list a list a.

Fixpoint filter_s {a : Set}
  (f : a bool) (l : list a) : list a :=
  match l with
  | [][]
  | x :: l
    let b := f x in
    let l := filter_s f l in
    if b then
      x :: l
    else
      l
  end.

Parameter rev_filter_es : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result (list a) trace.

Fixpoint filter_es {a trace : Set}
  (f : a Pervasives.result bool trace) (l : list a)
  : Pervasives.result (list a) trace :=
  match l with
  | []return? []
  | x :: l
    let? b := f x in
    let? l := filter_es f l in
    if b then
      return? (x :: l)
    else
      return? l
  end.

Parameter rev_filteri_e : {a trace : Set},
  (int a Pervasives.result bool trace) list a
  Pervasives.result (list a) trace.

Parameter filteri_e : {a trace : Set},
  (int a Pervasives.result bool trace) list a
  Pervasives.result (list a) trace.

Parameter rev_filteri_s : {a : Set},
  (int a bool) list a list a.

Parameter filteri_s : {a : Set},
  (int a bool) list a list a.

Parameter rev_filteri_es : {a trace : Set},
  (int a Pervasives.result bool trace) list a
  Pervasives.result (list a) trace.

Parameter filteri_es : {a trace : Set},
  (int a Pervasives.result bool trace) list a
  Pervasives.result (list a) trace.

Parameter filter_p : {a : Set},
  (a bool) list a list a.

Parameter rev_partition : {a : Set},
  (a bool) list a list a × list a.

Definition partition : {a : Set},
  (a bool) list a list a × list a :=
  fun _
  List.partition.

Parameter rev_partition_map : {a b c : Set},
  (a Either.t b c) list a list b × list c.

Parameter partition_map : {a b c : Set},
  (a Either.t b c) list a list b × list c.

Parameter rev_partition_result : {a b : Set},
  list (Pervasives.result a b) list a × list b.

Parameter partition_result : {a b : Set},
  list (Pervasives.result a b) list a × list b.

Parameter rev_partition_either : {a b : Set},
  list (Either.t a b) list a × list b.

Parameter partition_either : {a b : Set},
  list (Either.t a b) list a × list b.

Parameter rev_partition_e : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result (list a × list a) trace.

Parameter partition_e : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result (list a × list a) trace.

Parameter rev_partition_s : {a : Set},
  (a bool) list a list a × list a.

Fixpoint partition_s {a : Set}
  (f : a bool) (l : list a) : list a × list a :=
  match l with
  | []([], [])
  | x :: l
    let b := f x in
    let '(yes, no) := partition_s f l in
    if b then
      (x :: yes, no)
    else
    (yes, x :: no)
  end.

Parameter rev_partition_es : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result (list a × list a) trace.

Parameter partition_es : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result (list a × list a) trace.

Parameter partition_p : {a : Set},
  (a bool) list a list a × list a.

Parameter rev_partition_map_e : {a b c trace : Set},
  (a Pervasives.result (Either.t b c) trace) list a
  Pervasives.result (list b × list c) trace.

Parameter partition_map_e : {a b c trace : Set},
  (a Pervasives.result (Either.t b c) trace) list a
  Pervasives.result (list b × list c) trace.

Parameter rev_partition_map_s : {a b c : Set},
  (a Either.t b c) list a list b × list c.

Parameter partition_map_s : {a b c : Set},
  (a Either.t b c) list a list b × list c.

Parameter rev_partition_map_es : {a b c trace : Set},
  (a Pervasives.result (Either.t b c) trace) list a
  Pervasives.result (list b × list c) trace.

Parameter partition_map_es : {a b c trace : Set},
  (a Pervasives.result (Either.t b c) trace) list a
  Pervasives.result (list b × list c) trace.

Parameter iter : {a : Set}, (a unit) list a unit.

Fixpoint iter_e {a trace : Set}
  (f : a Pervasives.result unit trace) (l : list a)
  : Pervasives.result unit trace :=
  match l with
  | []return? tt
  | x :: l
    let? _ := f x in
    iter_e f l
  end.

Fixpoint iter_s {a : Set}
  (f : a unit) (l : list a) : unit :=
  match l with
  | []tt
  | x :: l
    let _ := f x in
    iter_s f l
  end.

Fixpoint iter_es {a trace : Set}
  (f : a Pervasives.result unit trace) (l : list a)
  : Pervasives.result unit trace :=
  match l with
  | []return? tt
  | x :: l
    let? _ := f x in
    iter_es f l
  end.

Parameter iter_p : {a : Set}, (a unit) list a unit.

Parameter iteri : {a : Set}, (int a unit) list a unit.

Parameter iteri_e : {a trace : Set},
  (int a Pervasives.result unit trace) list a
  Pervasives.result unit trace.

Parameter iteri_s : {a : Set},
  (int a unit) list a unit.

Parameter iteri_es : {a trace : Set},
  (int a Pervasives.result unit trace) list a
  Pervasives.result unit trace.

Parameter iteri_p : {a : Set},
  (int a unit) list a unit.

Definition map : {a b : Set}, (a b) list a list b :=
  @Lists.List.map.

Fixpoint map_e {a b trace : Set}
  (f : a Pervasives.result b trace) (l : list a)
  : Pervasives.result (list b) trace :=
  match l with
  | []return? []
  | x :: l
    let? y := f x in
    let? l' := map_e f l in
    return? (y :: l')
  end.

Fixpoint map_s {a b : Set}
  (f : a b) (l : list a) : list b :=
  match l with
  | [][]
  | x :: l
    let x := f x in
    let l := map_s f l in
    x :: l
  end.

Fixpoint map_es {a b trace : Set}
  (f : a Pervasives.result b trace) (l : list a)
  : Pervasives.result (list b) trace :=
  match l with
  | []return? []
  | x :: l
    let? y := f x in
    let? l' := map_es f l in
    return? (y :: l')
  end.

Parameter map_p : {a b : Set},
  (a b) list a list b.

Definition mapi : {a b : Set}, (int a b) list a list b :=
  fun _ _
  List.mapi.

Parameter mapi_e : {a b trace : Set},
  (int a Pervasives.result b trace) list a
  Pervasives.result (list b) trace.

Parameter mapi_s : {a b : Set},
  (int a b) list a list b.

Parameter mapi_es : {a b trace : Set},
  (int a Pervasives.result b trace) list a
  Pervasives.result (list b) trace.

Parameter mapi_p : {a b : Set},
  (int a b) list a list b.

Definition rev_map : {a b : Set}, (a b) list a list b :=
  fun _ _
  List.rev_map.

Parameter rev_mapi : {a b : Set}, (int a b) list a list b.

Parameter rev_map_e : {a b trace : Set},
  (a Pervasives.result b trace) list a
  Pervasives.result (list b) trace.

Parameter rev_map_s : {a b : Set},
  (a b) list a list b.

Parameter rev_map_es : {a b trace : Set},
  (a Pervasives.result b trace) list a
  Pervasives.result (list b) trace.

Parameter rev_map_p : {a b : Set},
  (a b) list a list b.

Parameter rev_mapi_e : {a b trace : Set},
  (int a Pervasives.result b trace) list a
  Pervasives.result (list b) trace.

Parameter rev_mapi_s : {a b : Set},
  (int a b) list a list b.

Parameter rev_mapi_es : {a b trace : Set},
  (int a Pervasives.result b trace) list a
  Pervasives.result (list b) trace.

Parameter rev_mapi_p : {a b : Set},
  (int a b) list a list b.

Parameter rev_filter_map : {a b : Set},
  (a option b) list a list b.

Parameter rev_filter_map_e : {a b trace : Set},
  (a Pervasives.result (option b) trace) list a
  Pervasives.result (list b) trace.

Parameter filter_map_e : {a b trace : Set},
  (a Pervasives.result (option b) trace) list a
  Pervasives.result (list b) trace.

Parameter rev_filter_map_s : {a b : Set},
  (a option b) list a list b.

Fixpoint filter_map {a b : Set} (f : a option b) (l : list a) : list b :=
  match l with
  | [][]
  | x :: l'
    match f x with
    | Nonefilter_map f l'
    | Some yy :: filter_map f l'
    end
  end.

Fixpoint filter_map_s {a b : Set}
  (f : a option b) (l : list a) : list b :=
  match l with
  | [][]
  | x :: l
    let y := f x in
    let l' := filter_map_s f l in
    match y with
    | Some yy :: l'
    | Nonel'
    end
  end.

Parameter rev_filter_map_es : {a b trace : Set},
  (a Pervasives.result (option b) trace) list a
  Pervasives.result (list b) trace.

Fixpoint filter_map_es {a b trace : Set}
  (f : a Pervasives.result (option b) trace) (l : list a)
  : Pervasives.result (list b) trace :=
  match l with
  | []return? []
  | x :: l
    let? y := f x in
    let? l' := filter_map_es f l in
    match y with
    | Some yreturn? (y :: l')
    | Nonereturn? l'
    end
  end.

Parameter filter_map_p : {a b : Set},
  (a option b) list a list b.

Parameter concat_map : {a b : Set}, (a list b) list a list b.

Parameter concat_map_s : {a b : Set},
  (a list b) list a list b.

Parameter concat_map_e : {_error a b : Set},
  (a Pervasives.result (list b) _error) list a
  Pervasives.result (list b) _error.

Parameter concat_map_es : {_error a b : Set},
  (a Pervasives.result (list b) _error) list a
  Pervasives.result (list b) _error.

Parameter concat_map_p : {a b : Set},
  (a list b) list a list b.

Definition fold_left : {a b : Set}, (a b a) a list b a :=
  fun _ _
  List.fold_left.

Definition fold_left_e {a b trace : Set}
  (f : a b Pervasives.result a trace) (acc : a) (l : list b) :
  Pervasives.result a trace :=
  fold_left (fun acc itemlet? acc := acc in f acc item) (return? acc) l.

Fixpoint fold_left_s {a b : Set}
  (f : a b a) (accumulator : a) (l : list b) : a :=
  match l with
  | []accumulator
  | x :: l
    let accumulator := f accumulator x in
    fold_left_s f accumulator l
  end.

Fixpoint fold_left_es {a b trace : Set}
  (f : a b Pervasives.result a trace) (accumulator : a)
  (l : list b) : Pervasives.result a trace :=
  match l with
  | []return? accumulator
  | x :: l
    let? accumulator := f accumulator x in
    fold_left_es f accumulator l
  end.

Parameter fold_left_map : {a b c : Set},
  (a b a × c) a list b a × list c.

Parameter fold_left_map_e : {a b c trace : Set},
  (a b Pervasives.result (a × c) trace) a list b
  Pervasives.result (a × list c) trace.

Parameter fold_left_map_s : {a b c : Set},
  (a b a × c) a list b a × list c.

Parameter fold_left_map_es : {a b c trace : Set},
  (a b Pervasives.result (a × c) trace) a list b
  Pervasives.result (a × list c) trace.

Definition fold_left_i {a b : Set}
  (f : int a b a) (acc : a) (l : list b) : a :=
  snd (
    fold_left
      (fun '(index, acc) item
        let acc := f index acc item in
        (index +i 1, acc)
      )
      (0, acc)
      l
  ).

Definition fold_left_i_e {a b trace : Set}
  (f : int a b Pervasives.result a trace) (acc : a) (l : list b) :
  Pervasives.result a trace :=
  fold_left_i
    (fun index acc itemlet? acc := acc in f index acc item)
    (return? acc)
    l.

Definition fold_left_i_s := @fold_left_i.
Arguments fold_left_i_s {a b}.

Definition fold_left_i_es := @fold_left_i_e.
Arguments fold_left_i_es {a b trace}.

Definition fold_right : {a b : Set}, (a b b) list a b b :=
  fun _ _
  List.fold_right.

Parameter fold_right_e : {a b trace : Set},
  (a b Pervasives.result b trace) list a b
  Pervasives.result b trace.

Fixpoint fold_right_s {a b : Set}
  (f : a b b) (l : list a) (accumulator : b) : b :=
  match l with
  | []accumulator
  | x :: l
    let accumulator := fold_right_s f l accumulator in
    f x accumulator
  end.

Fixpoint fold_right_es {a b trace : Set}
  (f : a b Pervasives.result b trace) (l : list a)
  (accumulator : b) : Pervasives.result b trace :=
  match l with
  | []return? accumulator
  | x :: l
    let? accumulator := fold_right_es f l accumulator in
    f x accumulator
  end.

Parameter iter2_e : {a b trace : Set},
  trace (a b Pervasives.result unit trace) list a list b
  Pervasives.result unit trace.

Parameter iter2_s : {a b trace : Set},
  trace (a b unit) list a list b
  Pervasives.result unit trace.

Parameter iter2_es : {a b trace : Set},
  trace (a b Pervasives.result unit trace) list a
  list b Pervasives.result unit trace.

Parameter map2_e : {a b c trace : Set},
  trace (a b Pervasives.result c trace) list a list b
  Pervasives.result (list c) trace.

Parameter map2_s : {a b c trace : Set},
  trace (a b c) list a list b
  Pervasives.result (list c) trace.

Parameter map2_es : {a b c trace : Set},
  trace (a b Pervasives.result c trace) list a
  list b Pervasives.result (list c) trace.

Parameter rev_map2_e : {a b c trace : Set},
  trace (a b Pervasives.result c trace) list a list b
  Pervasives.result (list c) trace.

Parameter rev_map2_s : {a b c trace : Set},
  trace (a b c) list a list b
  Pervasives.result (list c) trace.

Parameter rev_map2_es : {a b c trace : Set},
  trace (a b Pervasives.result c trace) list a
  list b Pervasives.result (list c) trace.

Parameter fold_left2_e : {a b c trace : Set},
  trace (a b c Pervasives.result a trace) a list b
  list c Pervasives.result a trace.

Parameter fold_left2_s : {a b c trace : Set},
  trace (a b c a) a list b list c
  Pervasives.result a trace.

Parameter fold_left2_es : {a b c trace : Set},
  trace (a b c Pervasives.result a trace) a
  list b list c Pervasives.result a trace.

Parameter fold_right2_e : {a b c trace : Set},
  trace (a b c Pervasives.result c trace) list a list b
  c Pervasives.result c trace.

Parameter fold_right2_s : {a b c trace : Set},
  trace (a b c c) list a list b c
  Pervasives.result c trace.

Parameter fold_right2_es : {a b c trace : Set},
  trace (a b c Pervasives.result c trace) list a
  list b c Pervasives.result c trace.

Definition for_all : {a : Set}, (a bool) list a bool :=
  fun a
  List.forallb (A := a).

Parameter for_all_e : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result bool trace.

Fixpoint for_all_s {a : Set}
  (f : a bool) (l : list a) : bool :=
  match l with
  | []true
  | x :: l
    let b := f x in
    if b then
      for_all_s f l
    else
      false
  end.

Parameter for_all_es : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result bool trace.

Parameter for_all_p : {a : Set},
  (a bool) list a bool.

Definition _exists : {a : Set}, (a bool) list a bool :=
  fun a
  List.existsb (A := a).

Parameter exists_e : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result bool trace.

Fixpoint exists_s {a : Set}
  (f : a bool) (l : list a) : bool :=
  match l with
  | []false
  | x :: l
    let b := f x in
    if b then
      true
    else
      exists_s f l
  end.

Parameter exists_es : {a trace : Set},
  (a Pervasives.result bool trace) list a
  Pervasives.result bool trace.

Parameter exists_p : {a : Set},
  (a bool) list a bool.

Parameter for_all2_e : {a b trace : Set},
  trace (a b Pervasives.result bool trace) list a list b
  Pervasives.result bool trace.

Parameter for_all2_s : {a b trace : Set},
  trace (a b bool) list a list b
  Pervasives.result bool trace.

Parameter for_all2_es : {a b trace : Set},
  trace (a b Pervasives.result bool trace) list a
  list b Pervasives.result bool trace.

Parameter exists2_e : {a b trace : Set},
  trace (a b Pervasives.result bool trace) list a list b
  Pervasives.result bool trace.

Parameter exists2_s : {a b trace : Set},
  trace (a b bool) list a list b
  Pervasives.result bool trace.

Parameter exists2_es : {a b trace : Set},
  trace (a b Pervasives.result bool trace) list a
  list b Pervasives.result bool trace.

Parameter combine_drop : {a b : Set}, list a list b list (a × b).

Parameter combine_with_leftovers : {a b : Set},
  list a list b list (a × b) × option (Either.t (list a) (list b)).

Parameter compare : {a : Set},
  (a a int) list a list a int.

Definition compare_lengths : {a b : Set}, list a list b int :=
  fun _ _ l1 l2
  (length l1) -i (length l2).

Definition compare_length_with : {a : Set}, list a int int :=
  fun _ l n
  length l -i n.

Fixpoint equal {a : Set} (eqb : a a bool) (l1 l2 : list a) : bool :=
  match l1, l2 with
  | [], []true
  | x1 :: l1, x2 :: l2eqb x1 x2 && equal eqb l1 l2
  | _, _false
  end.

Parameter sort : {a : Set}, (a a int) list a list a.

Parameter stable_sort : {a : Set}, (a a int) list a list a.

Parameter fast_sort : {a : Set}, (a a int) list a list a.

Parameter sort_uniq : {a : Set}, (a a int) list a list a.

Parameter to_seq : {a : Set}, list a Seq.t a.

Parameter of_seq : {a : Set}, Seq.t a list a.

Parameter init_ep : {_error a : Set},
  _error int (int M? a) M? (list a).

Parameter filter_ep : {a : Set},
  (a M? bool) list a M? (list a).

Parameter partition_ep : {a : Set},
  (a M? bool) list a M? (list a × list a).

Parameter partition_map_ep : {a b c : Set},
  (a M? (Either.t b c)) list a M? (list b × list c).

Parameter iter_ep : {a : Set},
  (a M? unit) list a M? unit.

Parameter iteri_ep : {a : Set},
  (int a M? unit) list a M? unit.

Parameter map_ep : {a b : Set},
  (a M? b) list a M? (list b).

Parameter mapi_ep : {a b : Set},
  (int a M? b) list a M? (list b).

Parameter rev_map_ep : {a b : Set},
  (a M? b) list a M? (list b).

Parameter rev_mapi_ep : {a b : Set},
  (int a M? b) list a M? (list b).

Parameter filter_map_ep : {a b : Set},
  (a M? (option b)) list a M? (list b).

Parameter concat_map_ep : {a b : Set},
  (a M? (list b)) list a M? (list b).

Parameter for_all_ep : {a : Set},
  (a M? bool) list a M? bool.

Parameter exists_ep : {a : Set},
  (a M? bool) list a M? bool.