		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-ident

Print an identifier.

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

The ident-aidentp guard ensures that the identifier contains an ACL2 string consisting of one or more characters satisfying grammar-character-p.

Definitions and Theorems

Function: print-ident

(defun print-ident (ident pstate)
  (declare (xargs :guard (and (identp ident)
                              (pristatep pstate))))
  (declare
       (xargs :guard (ident-aidentp ident (pristate->gcc pstate))))
  (let ((__function__ 'print-ident))
    (declare (ignorable __function__))
    (b* ((string (ident->unwrap ident))
         (chars (acl2::string=>nats string)))
      (print-chars chars pstate))))

Theorem: pristatep-of-print-ident

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

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

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

Theorem: print-ident-of-ident-fix-ident

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

Theorem: print-ident-ident-equiv-congruence-on-ident

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

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

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

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

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