		Search-engine friendly clone of the ACL2 documentation.

Std/util

Defmvtypes

Introduce type-prescription rules for a function that returns multiple values.

Defmvtypes is just a shorthand that allows you to quickly introduce type-prescription rules for a function that returns multiple values.

General form:

(defmvtypes fn return-types
   [:hyp   hyp]
   [:hints hints])

For example,

(defmvtypes foo
  (true-listp nil booleanp (and (consp x) (true-listp x))))

introduces three type-prescription rules:

(true-listp (mv-nth 0 (foo ...))
(booleanp (mv-nth 2 (foo ...))
(and (consp (mv-nth 3 (foo ...))) (true-listp (mv-nth 3 (foo ...))))

Usage and Arguments

Each of the return-types should either be a plain symbol like true-listp, or a term whose only free variable is pkg::x, where pkg is the package of fn.

The theorems introduced will be unconditional unless a :hyp argument is provided. For instance,

(defmvtypes foo
  (nil nil true-listp)
  :hyp (bar a b c))

Would result in:

(implies (bar a b c)
         (true-listp (mv-nth 2 (foo ...))))

The :hints argument can be used to specify custom ACL2::hints to use. The same hints are given to each theorem.

Interaction with force

Sometimes force can get in the way of proving nice, hypothesis-free type-prescription rules. To try to avoid this, by default defmvtypes automatically:

Disables forcing before submitting its theorems, then
Uses ACL2::computed-hints to re-enable force when goals are stable-under-simplification.

The hope is that this will generally prevent force from screwing up type-prescription theorems, but will allow it to be used when it would be useful to do so. If you do not want this behavior, you can suppress it by giving any :hints.