PTREE_IN_PTREE_CONV : conv
STRUCTURE
patriciaLib
SYNOPSIS
Conversion for evaluating applications of patricia$IN_PTREE.
DESCRIPTION
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
PTREE_CONV
HOL  Kananaskis-14