Translating abstract sorts.
Function:
(defun translate-abstract-types (abs) (declare (xargs :guard (symbol-listp abs))) (let ((acl2::__function__ 'translate-abstract-types)) (declare (ignorable acl2::__function__)) (b* ((abs (symbol-list-fix abs)) ((unless (consp abs)) nil) ((cons abs-hd abs-tl) abs) (name (translate-symbol abs-hd)) (first-abs (cons name (cons '" = z3.DeclareSort('" (cons name '("')" #\Newline)))))) (cons first-abs (translate-abstract-types abs-tl)))))
Theorem:
(defthm paragraphp-of-translate-abstract-types (b* ((translated (translate-abstract-types abs))) (paragraphp translated)) :rule-classes :rewrite)