PTREE_TRANSFORM_CONV
patriciaLib.PTREE_TRANSFORM_CONV : conv
Conversion for evaluating applications of patricia$TRANSFORM.
The conversion PTREE_TRANSFORM_CONV evaluates terms of the form
TRANSFORM f t where t is a well-formed Patricia tree (constructed by
patricia$Empty, patricia$Leaf and patricia$Branch) and f is map.
Failure
The conversion will fail if the supplied term is not a suitable
application of patricia$TRANSFORM.
Example
> patriciaLib.PTREE_TRANSFORM_CONV ``TRANSFORM ODD Empty``;
Exception- Type error in function application.
Function: patriciaLib.PTREE_TRANSFORM_CONV : conv -> conv
Argument: (Parse.Term [QUOTE " (*#loc 1 36*)TRANSFORM ODD Empty"])
: term
Reason: Can't unify term to term -> thm (Incompatible types)
Fail "Static Errors" raised
> patriciaLib.PTREE_TRANSFORM_CONV ``TRANSFORM ODD (Branch 0 0 (Leaf 3 2) (Leaf 2 1))``;
Exception- Type error in function application.
Function: patriciaLib.PTREE_TRANSFORM_CONV : conv -> conv
Argument:
(
Parse.Term
[
QUOTE
" (*#loc 1 36*)TRANSFORM ODD (Branch 0 0 (Leaf 3 2) (Leaf 2 1))"
]) : term
Reason: Can't unify term to term -> thm (Incompatible types)
Fail "Static Errors" raised