PTREE_EVERY_LEAF_CONV

patriciaLib.PTREE_EVERY_LEAF_CONV : conv

Conversion for evaluating applications of patricia$EVERY_LEAF.

The conversion PTREE_EVERY_LEAF_CONV evaluates terms of the form EVERY_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$EVERY_LEAF.

Example

> patriciaLib.PTREE_EVERY_LEAF_CONV ``EVERY_LEAF (=) Empty``;
Exception- Type error in function application.
   Function: patriciaLib.PTREE_EVERY_LEAF_CONV : conv -> conv
   Argument: (Parse.Term [QUOTE " (*#loc 1 37*)EVERY_LEAF (=) Empty"])
      : term
   Reason: Can't unify term to term -> thm (Incompatible types)
Fail "Static Errors" raised

> patriciaLib.PTREE_EVERY_LEAF_CONV ``EVERY_LEAF (\x y. (x < 3) ==> (y = 1)) (Branch 0 0 (Leaf 3 2) (Leaf 2 1))``;
Exception- Type error in function application.
   Function: patriciaLib.PTREE_EVERY_LEAF_CONV : conv -> conv
   Argument:
      (
      Parse.Term
      [
         QUOTE
         " (*#loc 1 37*)EVERY_LEAF (\\x y. (x < 3) ==> (y = 1)) (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_EVERY_LEAF_CONV ``EVERY_LEAF (\x y. x < 2) (Branch 0 0 (Leaf 3 2) (Leaf 2 1))``;
Exception- Type error in function application.
   Function: patriciaLib.PTREE_EVERY_LEAF_CONV : conv -> conv
   Argument:
      (
      Parse.Term
      [
         QUOTE
         " (*#loc 1 37*)EVERY_LEAF (\\x y. x < 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

See also

patriciaLib.PTREE_CONV