		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-fsuffix-option

Print an optional floating suffix.

Signature
(print-fsuffix-option fsuffix? pstate) → new-pstate
Arguments: fsuffix? — Guard (fsuffix-optionp fsuffix?).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

If there is no suffix, we print nothing.

Definitions and Theorems

Function: print-fsuffix-option

(defun print-fsuffix-option (fsuffix? pstate)
  (declare (xargs :guard (and (fsuffix-optionp fsuffix?)
                              (pristatep pstate))))
  (let ((__function__ 'print-fsuffix-option))
    (declare (ignorable __function__))
    (fsuffix-option-case fsuffix?
                         :some (print-fsuffix fsuffix?.val pstate)
                         :none (pristate-fix pstate))))

Theorem: pristatep-of-print-fsuffix-option

(defthm pristatep-of-print-fsuffix-option
  (b* ((new-pstate (print-fsuffix-option fsuffix? pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: pristate->gcc-of-print-fsuffix-option

(defthm pristate->gcc-of-print-fsuffix-option
  (b* ((?new-pstate (print-fsuffix-option fsuffix? pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-fsuffix-option-of-fsuffix-option-fix-fsuffix?

(defthm print-fsuffix-option-of-fsuffix-option-fix-fsuffix?
  (equal (print-fsuffix-option (fsuffix-option-fix fsuffix?)
                               pstate)
         (print-fsuffix-option fsuffix? pstate)))

Theorem: print-fsuffix-option-fsuffix-option-equiv-congruence-on-fsuffix?

(defthm
   print-fsuffix-option-fsuffix-option-equiv-congruence-on-fsuffix?
  (implies (fsuffix-option-equiv fsuffix? fsuffix?-equiv)
           (equal (print-fsuffix-option fsuffix? pstate)
                  (print-fsuffix-option fsuffix?-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-fsuffix-option-of-pristate-fix-pstate

(defthm print-fsuffix-option-of-pristate-fix-pstate
  (equal (print-fsuffix-option fsuffix? (pristate-fix pstate))
         (print-fsuffix-option fsuffix? pstate)))

Theorem: print-fsuffix-option-pristate-equiv-congruence-on-pstate

(defthm print-fsuffix-option-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-fsuffix-option fsuffix? pstate)
                  (print-fsuffix-option fsuffix? pstate-equiv)))
  :rule-classes :congruence)