Print a function specifier.
Function:
(defun print-fun-spec (funspec pstate) (declare (xargs :guard (and (fun-specp funspec) (pristatep pstate)))) (let ((__function__ 'print-fun-spec)) (declare (ignorable __function__)) (fun-spec-case funspec :inline (keyword-uscores-case funspec.uscores :none (print-astring "inline" pstate) :start (print-astring "__inline" pstate) :both (print-astring "__inline__" pstate)) :noreturn (print-astring "_Noreturn" pstate))))
Theorem:
(defthm pristatep-of-print-fun-spec (b* ((new-pstate (print-fun-spec funspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-fun-spec-of-fun-spec-fix-funspec (equal (print-fun-spec (fun-spec-fix funspec) pstate) (print-fun-spec funspec pstate)))
Theorem:
(defthm print-fun-spec-fun-spec-equiv-congruence-on-funspec (implies (fun-spec-equiv funspec funspec-equiv) (equal (print-fun-spec funspec pstate) (print-fun-spec funspec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-fun-spec-of-pristate-fix-pstate (equal (print-fun-spec funspec (pristate-fix pstate)) (print-fun-spec funspec pstate)))
Theorem:
(defthm print-fun-spec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-fun-spec funspec pstate) (print-fun-spec funspec pstate-equiv))) :rule-classes :congruence)