Pretty-print a tag declaration.
(pprint-tag-declon declon level) → lines
Function:
(defun pprint-tag-declon (declon level) (declare (xargs :guard (and (tag-declonp declon) (natp level)))) (let ((__function__ 'pprint-tag-declon)) (declare (ignorable __function__)) (tag-declon-case declon :struct (append (pprint-one-line (msg "struct ~@0 {" (pprint-ident declon.tag)) (lnfix level)) (pprint-struct-declon-list declon.members (1+ (lnfix level))) (pprint-one-line "};" (lnfix level))) :union (append (pprint-one-line (msg "union ~@0 {" (pprint-ident declon.tag)) (lnfix level)) (pprint-struct-declon-list declon.members (1+ (lnfix level))) (pprint-one-line "};" (lnfix level))) :enum (pprint-one-line (msg "enum ~@0 {,@1};" (pprint-ident declon.tag) (pprint-comma-sep (pprint-ident-list declon.enumerators))) (lnfix level)))))
Theorem:
(defthm msg-listp-of-pprint-tag-declon (b* ((lines (pprint-tag-declon declon level))) (msg-listp lines)) :rule-classes :rewrite)
Theorem:
(defthm pprint-tag-declon-of-tag-declon-fix-declon (equal (pprint-tag-declon (tag-declon-fix declon) level) (pprint-tag-declon declon level)))
Theorem:
(defthm pprint-tag-declon-tag-declon-equiv-congruence-on-declon (implies (tag-declon-equiv declon declon-equiv) (equal (pprint-tag-declon declon level) (pprint-tag-declon declon-equiv level))) :rule-classes :congruence)
Theorem:
(defthm pprint-tag-declon-of-nfix-level (equal (pprint-tag-declon declon (nfix level)) (pprint-tag-declon declon level)))
Theorem:
(defthm pprint-tag-declon-nat-equiv-congruence-on-level (implies (acl2::nat-equiv level level-equiv) (equal (pprint-tag-declon declon level) (pprint-tag-declon declon level-equiv))) :rule-classes :congruence)