----------------------------------------------------------------------
PTREE_IN_PTREE_CONV                                      (patriciaLib)
----------------------------------------------------------------------
PTREE_IN_PTREE_CONV : conv

SYNOPSIS
Conversion for evaluating applications of {patricia$IN_PTREE}.

DESCRIBE
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``;
> val it = |- 1 IN_PTREE <{}> <=> F: thm

- patriciaLib.PTREE_IN_PTREE_CONV ``3 IN_PTREE (Branch 0 0 (Leaf 3 ()) (Leaf 2 ()))``;
> val it = |- 3 IN_PTREE Branch 0 0 (Leaf 3 ()) (Leaf 2 ()) <=> T: thm


SEEALSO
patriciaLib.PTREE_CONV.

----------------------------------------------------------------------