		Search-engine friendly clone of the ACL2 documentation.

Aignet-comb-transforms

N-output-comb-transform->name

Signature
(n-output-comb-transform->name x) → name
Arguments: x — Guard (n-output-comb-transform-p x).
Returns: name — Type (stringp name).

Definitions and Theorems

Function: n-output-comb-transform->name

(defun n-output-comb-transform->name (x)
  (declare (xargs :guard (n-output-comb-transform-p x)))
  (let ((__function__ 'n-output-comb-transform->name))
    (declare (ignorable __function__))
    (case (tag (n-output-comb-transform-fix x))
      (:n-outputs-unreachability-config "N-output Unreachability")
      (:n-outputs-dom-supergates-sweep-config
           "N-output observability supergate sweep")
      (otherwise (comb-transform->name x)))))

Theorem: stringp-of-n-output-comb-transform->name

(defthm stringp-of-n-output-comb-transform->name
  (b* ((name (n-output-comb-transform->name x)))
    (stringp name))
  :rule-classes :type-prescription)