PTREE_IN_PTREE_CONV
patriciaLib.PTREE_IN_PTREE_CONV : conv
Conversion for evaluating applications of patricia$IN_PTREE.
The conversion PTREE_IN_PTREE_CONV evaluates terms of the form
n IN_PTREE t where t is a well-formed unit Patricia tree
(constructed by patricia$Empty, patricia$Leaf and patricia$Branch)
and n is a natural number literal.
Failure
The conversion will fail if the supplied term is not a suitable
application of patricia$IN_PTREE.
Example
> patriciaLib.PTREE_IN_PTREE_CONV ``1 IN_PTREE Empty``;
Exception- HOL_ERR
(at Conv.RAND_CONV:
at Conv.REWR_CONV: lhs of thm doesn't match term) raised
> patriciaLib.PTREE_IN_PTREE_CONV ``3 IN_PTREE (Branch 0 0 (Leaf 3 ()) (Leaf 2 ()))``;
Exception- HOL_ERR
(at Conv.RAND_CONV:
at Conv.REWR_CONV: lhs of thm doesn't match term) raised