(make-alist-fn-lst fn-lst) makes fn-lst a fast alist
(make-alist-fn-lst fn-lst) → fast-fn-lst
Function:
(defun make-alist-fn-lst (fn-lst) (declare (xargs :guard (func-listp fn-lst))) (let ((acl2::__function__ 'make-alist-fn-lst)) (declare (ignorable acl2::__function__)) (b* ((fn-lst (func-list-fix fn-lst)) ((unless (consp fn-lst)) nil) ((cons first rest) fn-lst) ((func f) first) (new-f (change-func f :flattened-formals (flatten-formals/returns f.formals) :flattened-returns (flatten-formals/returns f.returns)))) (cons (cons f.name new-f) (make-alist-fn-lst rest)))))
Theorem:
(defthm func-alistp-of-make-alist-fn-lst (b* ((fast-fn-lst (make-alist-fn-lst fn-lst))) (func-alistp fast-fn-lst)) :rule-classes :rewrite)