		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-const

Print a constant.

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

Definitions and Theorems

Function: print-const

(defun print-const (const pstate)
  (declare (xargs :guard (and (constp const)
                              (pristatep pstate))))
  (let ((__function__ 'print-const))
    (declare (ignorable __function__))
    (const-case const
                :int (print-iconst const.unwrap pstate)
                :float (print-fconst const.unwrap pstate)
                :enum (print-ident const.unwrap pstate)
                :char (print-cconst const.unwrap pstate))))

Theorem: pristatep-of-print-const

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

Theorem: print-const-of-const-fix-const

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

Theorem: print-const-const-equiv-congruence-on-const

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

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

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

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

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