1signature patricia_castsLib =
2sig
3
4  include Abbrev
5
6  type term_ptree = patriciaLib.term_ptree
7  type num = Arbnum.num
8
9  val dest_word_ptree : term -> num * term_ptree
10  val mk_word_ptree   : num * term_ptree -> term
11
12  val add_cast_ptree_compset : computeLib.compset -> unit
13  val cast_ptree_compset     : unit -> computeLib.compset
14  val CAST_PTREE_CONV        : conv
15
16  val Define_mk_word_ptree  : string * string -> num -> term_ptree -> thm * thm
17  val iDefine_mk_word_ptree : string * string -> int -> term_ptree -> thm * thm
18
19end
20