		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Irr-lstmt-gout

An irrelevant output for C loop statement generation.

Signature
(irr-lstmt-gout) → acl2::irr
Returns: acl2::irr — Type (lstmt-goutp acl2::irr).

This can be used as a dummy value of the type.

Definitions and Theorems

Function: irr-lstmt-gout

(defun irr-lstmt-gout nil
  (declare (xargs :guard t))
  (let ((__function__ 'irr-lstmt-gout))
    (declare (ignorable __function__))
    (make-lstmt-gout :stmt (irr-stmt)
                     :test-term nil
                     :body-term nil
                     :affect nil
                     :limit-body nil
                     :limit-all nil
                     :events nil
                     :thm-name nil
                     :thm-index 1
                     :names-to-avoid nil)))

Theorem: lstmt-goutp-of-irr-lstmt-gout

(defthm lstmt-goutp-of-irr-lstmt-gout
  (b* ((acl2::irr (irr-lstmt-gout)))
    (lstmt-goutp acl2::irr))
  :rule-classes :rewrite)