		Search-engine friendly clone of the ACL2 documentation.

More-returns

Prove additional return-value theorems about a defined function.

more-returns is a concise syntax for proving additional theorems about the return-values of your functions, using define's :returns-like syntax.

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 return-spec is as described in returns-specifiers and shares a name with one of the :returns from the define.

Note that any xdoc documentation strings within these return specifiers is ignored. You should usually put such documentation into the :returns specifier for the define, instead.