extracted/bindLists.ml

   1 open Preamble
   2
   3 open State
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Bool
  10
  11 open Nat
  12
  13 open List
  14
  15 open Setoids
  16
  17 open Relations
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Monad
  30
  31 open Bind_new
  32
  33 type ('b, 'e) bind_list = ('b, 'e List.list) Bind_new.bind_new
  34
  35 (** val dpi1__o__blist_from_list__o__inject :
  36     ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list)
  37     Bind_new.bind_new Types.sig0 **)
  38 let dpi1__o__blist_from_list__o__inject x4 =
  39   Bind_new.Bret x4.Types.dpi1
  40
  41 (** val eject__o__blist_from_list__o__inject :
  42     'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new
  43     Types.sig0 **)
  44 let eject__o__blist_from_list__o__inject x4 =
  45   Bind_new.Bret (Types.pi1 x4)
  46
  47 (** val blist_from_list__o__inject :
  48     'a2 List.list -> ('a1, 'a2 List.list) Bind_new.bind_new Types.sig0 **)
  49 let blist_from_list__o__inject x3 =
  50   Bind_new.Bret x3
  51
  52 (** val dpi1__o__blist_from_list :
  53     ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list)
  54     Bind_new.bind_new **)
  55 let dpi1__o__blist_from_list x3 =
  56   let l = x3.Types.dpi1 in Bind_new.Bret l
  57
  58 (** val eject__o__blist_from_list :
  59     'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new **)
  60 let eject__o__blist_from_list x3 =
  61   let l = Types.pi1 x3 in Bind_new.Bret l
  62
  63 (** val bappend :
  64     ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
  65 let bappend x =
  66   Obj.magic
  67     (Monad.m_bin_op (Monad.max_def Bind_new.bindNew) List.append
  68       (Obj.magic x))
  69
  70 open Option
  71
  72 open Extranat
  73
  74 open Div_and_mod
  75
  76 open Util
  77
  78 open Vector
  79
  80 (** val bcons : 'a2 -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
  81 let bcons e =
  82   Obj.magic
  83     (Monad.m_map (Monad.max_def Bind_new.bindNew) (fun x -> List.Cons (e,
  84       x)))
  85
  86 open Lists
  87