Module Isa_btree.Isa_export_wrapper

module Isa_export_assert_flag : sig ... end

Control isabelle assert flag

include Isa_export_assert_flag
val enable_isa_checks : unit -> unit
val disable_isa_checks : unit -> unit

Leaf stream implementation

module Internal_leaf_stream_impl : sig ... end

Conversions between Isabelle types and OCaml types

module Internal_conversions : sig ... end
module Internal1 : sig ... end
val wf_tree : cs:Isa_btree__.Constants_type.constants -> ms:Isa_export.Tree.min_size_t option -> k_cmp:('a -> 'a -> int) -> ('a'b) Isa_export.Tree.tree -> bool
module Internal_make_with_k_maps : sig ... end

This is the most general implementation, where we just require k_cmp and map implementations

include Internal_make_with_k_maps
type ('k, 'v, 'r, 't, 'leaf, 'node, 'leaf_stream, 'store_ops) t2 = {
leaf_ops : ('k'v'leaf) Isa_btree_intf.leaf_ops;
node_ops : ('k'r'node) Isa_btree_intf.node_ops;
rest : store_ops:'store_ops -> ('k'v'r't'leaf'node'leaf_stream) Isa_btree_intf.Pre_btree_ops_type.pre_btree_ops;
}
val make_with_k_maps : monad_ops:'t Tjr_monad.monad_ops -> cs:Isa_btree__.Constants_type.constants -> k_cmp:('k -> 'k -> int) -> k_map:('k'v'leaf) Isa_btree_intf.Leaf_node_frame_map_ops_type.map_ops -> kopt_map:('k option'r'node) Isa_btree_intf.Leaf_node_frame_map_ops_type.map_ops -> dbg_tree_at_r:('r -> (unit, 't) Tjr_monad.m) -> ('k'v'r't'leaf'node('r'leaf('k'r'node) Isa_btree_intf.Frame_type.frame) Internal_leaf_stream_impl._t('r('node'leaf) Isa_btree__Isa_export.Disk_node.dnode't) Isa_btree_intf.store_ops) t2
val make_with_k_maps : monad_ops:'a Tjr_monad.monad_ops -> cs:Isa_btree__.Constants_type.constants -> k_cmp:('b -> 'b -> int) -> k_map:('b'c'd) Isa_btree_intf.Leaf_node_frame_map_ops_type.map_ops -> kopt_map:('b option'e'f) Isa_btree_intf.Leaf_node_frame_map_ops_type.map_ops -> dbg_tree_at_r:('e -> (unit, 'a) Tjr_monad.m) -> ('b'c'e'a'd'f('e'd('b'e'f) Isa_btree_intf.frame) Isa_btree__Isa_btree_intf.Internal_leaf_stream_impl_t._t('e('f'd) Isa_btree_intf.dnode'a) Isa_btree_intf.store_ops) t2