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