Included Books
other
(in-package "ACL2")
include-book
(include-book "add-io-pairs")
gfunction
(defun g (x y) (declare (xargs :guard (and (natp x) (natp y)))) (mv (non-exec (* 10 x)) (* 10 y)))
other
(add-io-pair (g 100 200) (mv 1000 2000))