PTREE_SIZE_CONV : conv
STRUCTURE
patriciaLib
SYNOPSIS
Conversion for evaluating applications of patricia$SIZE.
DESCRIPTION
The conversion PTREE_SIZE_CONV evaluates terms of the form SIZE 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$SIZE.
EXAMPLE
- patriciaLib.PTREE_SIZE_CONV ``SIZE Empty``;
> val it = |- SIZE <{}> = 0: thm

- patriciaLib.PTREE_SIZE_CONV ``SIZE (Branch 0 0 (Leaf 3 2) (Leaf 2 1))``;
> val it = |- SIZE (Branch 0 0 (Leaf 3 2) (Leaf 2 1)) = 2: thm
SEEALSO
PTREE_CONV
HOL  Trindemossen-1