blob: 2f570490f5c0eba61257e73619a221d5a95d116b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
(* ========================================================================== *)
(* DYNAMIC LOOKUP TREES (HOL Zero) *)
(* - Library support for data storage in dynamic indexed binary trees *)
(* *)
(* By Mark Adams *)
(* Copyright (c) Proof Technologies Ltd, 2008-2011 *)
(* ========================================================================== *)
module type Dltree_sig = sig
type ('a,'b) dltree
val dltree_empty : unit -> ('a,'b) dltree
val dltree_reempty : ('a,'b) dltree -> unit
val dltree_mem : 'a -> ('a,'b) dltree -> bool
val dltree_lookup : 'a -> ('a,'b) dltree -> 'b
val dltree_elem : 'a -> ('a,'b) dltree -> 'a * 'b
val dltree_elems : ('a,'b) dltree -> ('a * 'b) list
val dltree_insert : ('a * 'b) -> ('a,'b) dltree -> unit
val dltree_remove : 'a -> ('a,'b) dltree -> unit
end;;
|
