extracted/bindLists.mli

   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) Bind_new.bind_new
  37   Types.sig0
  38
  39 val eject__o__blist_from_list__o__inject :
  40   'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new
  41   Types.sig0
  42
  43 val blist_from_list__o__inject :
  44   'a2 List.list -> ('a1, 'a2 List.list) Bind_new.bind_new Types.sig0
  45
  46 val dpi1__o__blist_from_list :
  47   ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list) Bind_new.bind_new
  48
  49 val eject__o__blist_from_list :
  50   'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new
  51
  52 val bappend :
  53   ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list
  54
  55 open Option
  56
  57 open Extranat
  58
  59 open Div_and_mod
  60
  61 open Util
  62
  63 open Vector
  64
  65 val bcons : 'a2 -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list
  66
  67 open Lists
  68