----------------------------------------------------------------------
PTREE_ADD_CONV                                           (patriciaLib)
----------------------------------------------------------------------
PTREE_ADD_CONV : conv

SYNOPSIS
Conversion for evaluating applications of {patricia$ADD} and {patricia$ADD_LIST}.

DESCRIBE
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
patriciaLib.PTREE_CONV.

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