Discriminate
between a
This is used by
abstract-bin-val-rest,
abstract-dec-val-rest, and
abstract-hex-val-rest
to distinguish between the two alternatives
in the definiens of
Function:
(defun abstract-bin/dec/hex-val-rest-dot-p (tree) (declare (xargs :guard (treep tree))) (b* (((fun (fail)) (abstract-fail)) ((unless (tree-case tree :nonleaf)) (fail)) (treess (tree-nonleaf->branches tree)) ((unless (consp treess)) (fail)) (trees (car treess)) ((unless (consp trees)) (fail)) (subtree (car trees))) (equal subtree (tree-leafterm (list (char-code #\.))))))
Theorem:
(defthm booleanp-of-abstract-bin/dec/hex-val-rest-dot-p (b* ((yes/no (abstract-bin/dec/hex-val-rest-dot-p tree))) (booleanp yes/no)) :rule-classes :rewrite)