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.
(defmvtypes fn return-types [:hyp hyp] [:hints hints])
(defmvtypes foo (true-listp nil booleanp (and (consp x) (true-listp x))))
introduces three type-prescription rules:
Each of the
The theorems introduced will be unconditional unless a
(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 ...))))
Sometimes force can get in the way of proving nice, hypothesis-free
type-prescription rules. To try to avoid this, by default
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