Module Isa_btree.Isa_export_wrapper
module Isa_export_assert_flag : sig ... end
Control isabelle assert flag
include Isa_export_assert_flag
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