		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-standardp

Fun-spec-standardp

Signature
(fun-spec-standardp fun-spec) → fty::result
Arguments: fun-spec — Guard (fun-specp fun-spec).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: fun-spec-standardp

(defun fun-spec-standardp (fun-spec)
 (declare (xargs :guard (fun-specp fun-spec)))
 (declare (ignorable fun-spec))
 (let ((__function__ 'fun-spec-standardp))
  (declare (ignorable __function__))
  (fun-spec-case
   fun-spec
   :inline (keyword-uscores-case (fun-spec-inline->uscores fun-spec)
                                 :none)
   :noreturn t)))

Theorem: booleanp-of-fun-spec-standardp

(defthm booleanp-of-fun-spec-standardp
  (b* ((fty::result (fun-spec-standardp fun-spec)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: fun-spec-standardp-of-fun-spec-fix-fun-spec

(defthm fun-spec-standardp-of-fun-spec-fix-fun-spec
  (equal (fun-spec-standardp (fun-spec-fix fun-spec))
         (fun-spec-standardp fun-spec)))

Theorem: fun-spec-standardp-fun-spec-equiv-congruence-on-fun-spec

(defthm fun-spec-standardp-fun-spec-equiv-congruence-on-fun-spec
  (implies (fun-spec-equiv fun-spec fun-spec-equiv)
           (equal (fun-spec-standardp fun-spec)
                  (fun-spec-standardp fun-spec-equiv)))
  :rule-classes :congruence)