extracted/foldStuff.ml

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Bool
  10
  11 open Relations
  12
  13 open Nat
  14
  15 open Hints_declaration
  16
  17 open Core_notation
  18
  19 open Pts
  20
  21 open Logic
  22
  23 open Types
  24
  25 open List
  26
  27 open Util
  28
  29 (** val foldl_strong_internal :
  30     'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
  31     'a2) -> 'a1 List.list -> 'a1 List.list -> 'a2 -> 'a2 **)
  32 let rec foldl_strong_internal l h prefix suffix acc =
  33   (match suffix with
  34    | List.Nil ->
  35      (fun _ -> Util.eq_rect_Type0_r prefix acc (List.append prefix List.Nil))
  36    | List.Cons (hd, tl) ->
  37      (fun _ ->
  38        Logic.eq_coerc
  39          (foldl_strong_internal l h
  40            (List.append prefix (List.Cons (hd, List.Nil))) tl
  41            (h prefix hd tl __ acc)))) __
  42
  43 (** val foldl_strong :
  44     'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
  45     'a2) -> 'a2 -> 'a2 **)
  46 let foldl_strong l h acc =
  47   foldl_strong_internal l h List.Nil l acc
  48
  49 (** val foldr_strong_internal :
  50     'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
  51     'a2) -> 'a1 List.list -> 'a1 List.list -> 'a2 -> 'a2 **)
  52 let rec foldr_strong_internal l h prefix suffix acc =
  53   (match suffix with
  54    | List.Nil -> (fun _ -> acc)
  55    | List.Cons (hd, tl) ->
  56      (fun _ ->
  57        h prefix hd tl __
  58          (foldr_strong_internal l h
  59            (List.append prefix (List.Cons (hd, List.Nil))) tl acc))) __
  60
  61 (** val foldr_strong :
  62     'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
  63     'a2) -> 'a2 -> 'a2 **)
  64 let foldr_strong l h acc =
  65   foldr_strong_internal l h List.Nil l acc
  66