Prove additional return-value theorems about a defined function.
Example within a define:
(define my-make-alist (keys) :returns (alist alistp) (if (atom keys) nil (cons (cons (car keys) nil) (my-make-alist (cdr keys)))) /// (more-returns ;; no name needed since we're in a define (alist true-listp :rule-classes :type-prescription) (alist (equal (len alist) (len keys)) :name len-of-my-make-alist)))
Example outside a define:
(local (in-theory (enable my-make-alist))) (more-returns my-make-alist (alist (equal (strip-cars alist) (list-fix keys)) :name strip-cars-of-my-make-alist))
General form:
(more-returns [name] ;; defaults to the current define <return-spec-1> <return-spec-2> ...)
Where each
Note that any xdoc documentation strings within these return
specifiers is ignored. You should usually put such documentation into the