PTREE_ADD_CONV : conv
STRUCTURE
patriciaLib
SYNOPSIS
Conversion for evaluating applications of patricia$ADD and patricia$ADD_LIST.
DESCRIPTION
The conversion PTREE_ADD_CONV evaluates terms of the form t |+ (m,n) or t |++ l where t is a well-formed Patricia tree (correctly constructed using patricia$Empty, patricia$Leaf and patricia$Branch) and m is a natural number literal.
FAILURE
The conversion will fail if the supplied term is not a suitable application of patricia$ADD or patricia$ADD_LIST.
EXAMPLE
- patriciaLib.PTREE_ADD_CONV ``Empty |+ (3, x:num)``;
> val it = |- <{}> |+ (3,x) = Leaf 3 x: thm

- DEPTH_CONV patriciaLib.PTREE_ADD_CONV ``Empty |+ (3, 2) |+ (2,1)``;
> val it = |- <{}> |+ (3,2) |+ (2,1) = Branch 0 0 (Leaf 3 2) (Leaf 2 1): thm
SEEALSO
PTREE_CONV
HOL  Kananaskis-14