Add-io-pair
Speed up a function using a verified input-output pair
Add-io-pair is just a convenient abbreviation for add-io-pairs in the case of a single input-output pair. See add-io-pairs.
Examples:
(add-io-pair (f 3) '(3 . 3))
(add-io-pair (g 3 4) (mv 30 40))
(add-io-pair
(primep (primes::bn-254-group-prime)) t
:test eql
:hints (("Goal"
:in-theory
(enable primes::primep-of-bn-254-group-prime-constant))))
General Form:
(add-io-pair fn input output &key hints test debug verbose)
where fn is a guard-verified function symbol whose arguments do
not include state or any user-defined stobj. The arguments to
the macro are not evaluated.
Add-io-pair is merely a convenient way to invoke the utility add-io-pairs when there is a single input/output pair; see add-io-pairs for further documentation, including discussion of the
keywords (which are optional).
