		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-numeral

Abstract a numeral to a natural number.

Signature
(abs-numeral tree) → nat
Arguments: tree — Guard (abnf::treep tree).
Returns: nat — Type (nat-resultp nat).

Definitions and Theorems

Function: abs-numeral

(defun abs-numeral (tree)
  (declare (xargs :guard (abnf::treep tree)))
  (let ((__function__ 'abs-numeral))
    (declare (ignorable __function__))
    (b* (((okf sub)
          (abnf::check-tree-nonleaf-1 tree "numeral"))
         ((unless (consp sub))
          (reserrf (list :empty-numeral))))
      (abs-*-decimal-digit-to-nat sub))))

Theorem: nat-resultp-of-abs-numeral

(defthm nat-resultp-of-abs-numeral
  (b* ((nat (abs-numeral tree)))
    (nat-resultp nat))
  :rule-classes :rewrite)

Theorem: abs-numeral-of-tree-fix-tree

(defthm abs-numeral-of-tree-fix-tree
  (equal (abs-numeral (abnf::tree-fix tree))
         (abs-numeral tree)))

Theorem: abs-numeral-tree-equiv-congruence-on-tree

(defthm abs-numeral-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (abs-numeral tree)
                  (abs-numeral tree-equiv)))
  :rule-classes :congruence)