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