		Search-engine friendly clone of the ACL2 documentation.

Fun-sinfo

Fun-sinfo->inputs

Get the inputs field from a fun-sinfo.

Signature
(fun-sinfo->inputs x) → inputs
Arguments: x — Guard (fun-sinfop x).
Returns: inputs — Type (type-listp inputs).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: fun-sinfo->inputs$inline

(defun fun-sinfo->inputs$inline (x)
  (declare (xargs :guard (fun-sinfop x)))
  (declare (xargs :guard t))
  (let ((__function__ 'fun-sinfo->inputs))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x)))
           (type-list-fix (cdr (std::da-nth 0 x))))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: type-listp-of-fun-sinfo->inputs

(defthm type-listp-of-fun-sinfo->inputs
  (b* ((inputs (fun-sinfo->inputs$inline x)))
    (type-listp inputs))
  :rule-classes :rewrite)

Theorem: fun-sinfo->inputs$inline-of-fun-sinfo-fix-x

(defthm fun-sinfo->inputs$inline-of-fun-sinfo-fix-x
  (equal (fun-sinfo->inputs$inline (fun-sinfo-fix x))
         (fun-sinfo->inputs$inline x)))

Theorem: fun-sinfo->inputs$inline-fun-sinfo-equiv-congruence-on-x

(defthm fun-sinfo->inputs$inline-fun-sinfo-equiv-congruence-on-x
  (implies (fun-sinfo-equiv x x-equiv)
           (equal (fun-sinfo->inputs$inline x)
                  (fun-sinfo->inputs$inline x-equiv)))
  :rule-classes :congruence)