extracted/bind_new.mli

   1 open Preamble
   2
   3 open Jmeq
   4
   5 open Russell
   6
   7 open Bool
   8
   9 open Nat
  10
  11 open List
  12
  13 open Setoids
  14
  15 open Relations
  16
  17 open Hints_declaration
  18
  19 open Core_notation
  20
  21 open Pts
  22
  23 open Logic
  24
  25 open Types
  26
  27 open Monad
  28
  29 type ('b, 'e) bind_new =
  30 | Bret of 'e
  31 | Bnew of ('b -> ('b, 'e) bind_new)
  32
  33 val bind_new_rect_Type4 :
  34   ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  35   ('a1, 'a2) bind_new -> 'a3
  36
  37 val bind_new_rect_Type3 :
  38   ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  39   ('a1, 'a2) bind_new -> 'a3
  40
  41 val bind_new_rect_Type2 :
  42   ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  43   ('a1, 'a2) bind_new -> 'a3
  44
  45 val bind_new_rect_Type1 :
  46   ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  47   ('a1, 'a2) bind_new -> 'a3
  48
  49 val bind_new_rect_Type0 :
  50   ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  51   ('a1, 'a2) bind_new -> 'a3
  52
  53 val bind_new_inv_rect_Type4 :
  54   ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
  55   -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3
  56
  57 val bind_new_inv_rect_Type3 :
  58   ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
  59   -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3
  60
  61 val bind_new_inv_rect_Type2 :
  62   ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
  63   -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3
  64
  65 val bind_new_inv_rect_Type1 :
  66   ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
  67   -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3
  68
  69 val bind_new_inv_rect_Type0 :
  70   ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
  71   -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3
  72
  73 val bind_new_discr : ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __
  74
  75 val bind_new_jmdiscr : ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __
  76
  77 val bnews :
  78   Nat.nat -> ('a1 List.list -> ('a1, 'a2) bind_new) -> ('a1, 'a2) bind_new
  79
  80 val bnews_strong :
  81   Nat.nat -> ('a1 List.list -> __ -> ('a1, 'a2) bind_new) -> ('a1, 'a2)
  82   bind_new
  83
  84 val bbind :
  85   ('a1, 'a2) bind_new -> ('a2 -> ('a1, 'a3) bind_new) -> ('a1, 'a3) bind_new
  86
  87 val bindNew : Monad.monadProps
  88
  89 open State
  90
  91 val bcompile :
  92   'a2 Monad.smax_def__o__monad -> ('a2, 'a3) bind_new -> 'a3
  93   Monad.smax_def__o__monad
  94