		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-fsuffix

Print a floating suffix.

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

Definitions and Theorems

Function: print-fsuffix

(defun print-fsuffix (fsuffix pstate)
  (declare (xargs :guard (and (fsuffixp fsuffix)
                              (pristatep pstate))))
  (let ((__function__ 'print-fsuffix))
    (declare (ignorable __function__))
    (fsuffix-case
         fsuffix
         :locase-f (print-astring "f" pstate)
         :upcase-f (print-astring "F" pstate)
         :locase-l (print-astring "l" pstate)
         :upcase-l (print-astring "L" pstate)
         :locase-f16
         (b* ((pstate (print-astring "f16" pstate))
              (pstate (if fsuffix.x (print-astring "x" pstate)
                        pstate)))
           pstate)
         :locase-f32
         (b* ((pstate (print-astring "f32" pstate))
              (pstate (if fsuffix.x (print-astring "x" pstate)
                        pstate)))
           pstate)
         :locase-f64
         (b* ((pstate (print-astring "f64" pstate))
              (pstate (if fsuffix.x (print-astring "x" pstate)
                        pstate)))
           pstate)
         :locase-f128
         (b* ((pstate (print-astring "f128" pstate))
              (pstate (if fsuffix.x (print-astring "x" pstate)
                        pstate)))
           pstate)
         :upcase-f16
         (b* ((pstate (print-astring "F16" pstate))
              (pstate (if fsuffix.x (print-astring "x" pstate)
                        pstate)))
           pstate)
         :upcase-f32
         (b* ((pstate (print-astring "F32" pstate))
              (pstate (if fsuffix.x (print-astring "x" pstate)
                        pstate)))
           pstate)
         :upcase-f64
         (b* ((pstate (print-astring "F64" pstate))
              (pstate (if fsuffix.x (print-astring "x" pstate)
                        pstate)))
           pstate)
         :upcase-f128
         (b* ((pstate (print-astring "F128" pstate))
              (pstate (if fsuffix.x (print-astring "x" pstate)
                        pstate)))
           pstate))))

Theorem: pristatep-of-print-fsuffix

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

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

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

Theorem: print-fsuffix-of-fsuffix-fix-fsuffix

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

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

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

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

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

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

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