PTREE_DEPTH_CONV
patriciaLib.PTREE_DEPTH_CONV : conv
Conversion for evaluating applications of patricia$DEPTH.
The conversion PTREE_DEPTH_CONV evaluates terms of the form DEPTH t
where t is a well-formed Patricia tree (constructed by
patricia$Empty, patricia$Leaf and patricia$Branch).
Failure
The conversion will fail if the supplied term is not a suitable
application of patricia$DEPTH.
Example
> patriciaLib.PTREE_DEPTH_CONV ``DEPTH Empty``;
val it = ⊢ DEPTH <{}> = 0: thm
> patriciaLib.PTREE_DEPTH_CONV ``DEPTH (Branch 0 0 (Leaf 3 2) (Leaf 2 1))``;
val it = ⊢ DEPTH (Branch 0 0 (Leaf 3 2) (Leaf 2 1)) = 2: thm