		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-fconst

Print a floating constant.

Signature
(print-fconst fconst pstate) → new-pstate
Arguments: fconst — Guard (fconstp fconst).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

Definitions and Theorems

Function: print-fconst

(defun print-fconst (fconst pstate)
  (declare (xargs :guard (and (fconstp fconst)
                              (pristatep pstate))))
  (let ((__function__ 'print-fconst))
    (declare (ignorable __function__))
    (fconst-case
         fconst :dec
         (b* ((pstate (print-dec-core-fconst fconst.core pstate))
              (pstate (print-fsuffix-option fconst.suffix? pstate)))
           pstate)
         :hex
         (b* ((pstate (print-hprefix fconst.prefix pstate))
              (pstate (print-hex-core-fconst fconst.core pstate))
              (pstate (print-fsuffix-option fconst.suffix? pstate)))
           pstate))))

Theorem: pristatep-of-print-fconst

(defthm pristatep-of-print-fconst
  (b* ((new-pstate (print-fconst fconst pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-fconst-of-fconst-fix-fconst

(defthm print-fconst-of-fconst-fix-fconst
  (equal (print-fconst (fconst-fix fconst)
                       pstate)
         (print-fconst fconst pstate)))

Theorem: print-fconst-fconst-equiv-congruence-on-fconst

(defthm print-fconst-fconst-equiv-congruence-on-fconst
  (implies (fconst-equiv fconst fconst-equiv)
           (equal (print-fconst fconst pstate)
                  (print-fconst fconst-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-fconst-of-pristate-fix-pstate

(defthm print-fconst-of-pristate-fix-pstate
  (equal (print-fconst fconst (pristate-fix pstate))
         (print-fconst fconst pstate)))

Theorem: print-fconst-pristate-equiv-congruence-on-pstate

(defthm print-fconst-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-fconst fconst pstate)
                  (print-fconst fconst pstate-equiv)))
  :rule-classes :congruence)