/usr/share/acl2-6.3/books/cutil/look-up.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((4 RECORD-EXPANSION (DEFSECTION CUTIL::VAR-IS-STOBJ-P :PARENTS (CUTIL::SUPPORT) :SHORT "@(call var-is-stobj-p) checks whether @('var') is currently the name
of a @(see acl2::stobj)." (DEFUND CUTIL::VAR-IS-STOBJ-P (CUTIL::VAR WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::VAR) (PLIST-WORLDP WORLD)))) (CONSP (GETPROP CUTIL::VAR (QUOTE STOBJ) NIL (QUOTE CUTIL::CURRENT-ACL2-WORLD) WORLD))) (LOCAL (PROGN (ASSERT! (NOT (CUTIL::VAR-IS-STOBJ-P (QUOTE CUTIL::FOO) (W STATE)))) (ASSERT! (CUTIL::VAR-IS-STOBJ-P (QUOTE STATE) (W STATE))) (DEFSTOBJ CUTIL::FOO (CUTIL::FIELD1 :INITIALLY 0)) (ASSERT! (CUTIL::VAR-IS-STOBJ-P (QUOTE CUTIL::FOO) (W STATE)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::VAR-IS-STOBJ-P)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::VAR-IS-STOBJ-P (CUTIL::VAR WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::VAR) (PLIST-WORLDP WORLD)))) (CONSP (GETPROP CUTIL::VAR (QUOTE STOBJ) NIL (QUOTE CUTIL::CURRENT-ACL2-WORLD) WORLD))) (LOCAL (PROGN (ASSERT! (NOT (CUTIL::VAR-IS-STOBJ-P (QUOTE CUTIL::FOO) (W STATE)))) (ASSERT! (CUTIL::VAR-IS-STOBJ-P (QUOTE STATE) (W STATE))) (DEFSTOBJ CUTIL::FOO (CUTIL::FIELD1 :INITIALLY 0)) (ASSERT! (CUTIL::VAR-IS-STOBJ-P (QUOTE CUTIL::FOO) (W STATE))))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::VAR-IS-STOBJ-P (CUTIL::VAR WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::VAR) (PLIST-WORLDP WORLD)))) (CONSP (GETPROP CUTIL::VAR (QUOTE STOBJ) NIL (QUOTE CUTIL::CURRENT-ACL2-WORLD) WORLD))) (RECORD-EXPANSION (LOCAL (PROGN (ASSERT! (NOT (CUTIL::VAR-IS-STOBJ-P (QUOTE CUTIL::FOO) (W STATE)))) (ASSERT! (CUTIL::VAR-IS-STOBJ-P (QUOTE STATE) (W STATE))) (DEFSTOBJ CUTIL::FOO (CUTIL::FIELD1 :INITIALLY 0)) (ASSERT! (CUTIL::VAR-IS-STOBJ-P (QUOTE CUTIL::FOO) (W STATE))))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE CUTIL::VAR-IS-STOBJ-P)) (XDOC::PARENTS (QUOTE (CUTIL::SUPPORT))) (XDOC::SHORT (QUOTE "@(call var-is-stobj-p) checks whether @('var') is currently the name
of a @(see acl2::stobj).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::VAR-IS-STOBJ-P))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::VAR-IS-STOBJ-P) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::SUPPORT) (:SHORT . "@(call var-is-stobj-p) checks whether @('var') is currently the name
of a @(see acl2::stobj).") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |CUTIL|::|VAR-IS-STOBJ-P|)") (:FROM . "[books]/cutil/look-up.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::VAR-IS-STOBJ-P)))))) (VALUE-TRIPLE (QUOTE CUTIL::VAR-IS-STOBJ-P))))) (5 RECORD-EXPANSION (DEFSECTION CUTIL::LOOK-UP-FORMALS :PARENTS (CUTIL::SUPPORT) :SHORT "@(call look-up-formals) looks up the names of the arguments of the
function @('fn'), or causes a hard error if @('fn') isn't a function." (DEFUND CUTIL::LOOK-UP-FORMALS (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOOK-UP-FORMALS)) (CUTIL::LOOK (GETPROP CUTIL::FN (QUOTE FORMALS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((WHEN (EQ CUTIL::LOOK :BAD)) (RAISE "Can't look up the formals for ~x0!" CUTIL::FN)) ((UNLESS (SYMBOL-LISTP CUTIL::LOOK)) (RAISE "Expected a symbol-listp, but found ~x0!" CUTIL::LOOK))) CUTIL::LOOK)) (LOCAL (IN-THEORY (ENABLE CUTIL::LOOK-UP-FORMALS))) (DEFTHM CUTIL::SYMBOL-LISTP-OF-LOOK-UP-FORMALS (SYMBOL-LISTP (CUTIL::LOOK-UP-FORMALS CUTIL::FN WORLD))) (LOCAL (PROGN (ASSERT! (EQUAL (CUTIL::LOOK-UP-FORMALS (QUOTE CUTIL::LOOK-UP-FORMALS) (W STATE)) (QUOTE (CUTIL::FN WORLD))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::LOOK-UP-FORMALS)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::LOOK-UP-FORMALS (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOOK-UP-FORMALS)) (CUTIL::LOOK (GETPROP CUTIL::FN (QUOTE FORMALS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((WHEN (EQ CUTIL::LOOK :BAD)) (RAISE "Can't look up the formals for ~x0!" CUTIL::FN)) ((UNLESS (SYMBOL-LISTP CUTIL::LOOK)) (RAISE "Expected a symbol-listp, but found ~x0!" CUTIL::LOOK))) CUTIL::LOOK)) (LOCAL (IN-THEORY (ENABLE CUTIL::LOOK-UP-FORMALS))) (DEFTHM CUTIL::SYMBOL-LISTP-OF-LOOK-UP-FORMALS (SYMBOL-LISTP (CUTIL::LOOK-UP-FORMALS CUTIL::FN WORLD))) (LOCAL (PROGN (ASSERT! (EQUAL (CUTIL::LOOK-UP-FORMALS (QUOTE CUTIL::LOOK-UP-FORMALS) (W STATE)) (QUOTE (CUTIL::FN WORLD)))))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::LOOK-UP-FORMALS (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOOK-UP-FORMALS)) (CUTIL::LOOK (GETPROP CUTIL::FN (QUOTE FORMALS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((WHEN (EQ CUTIL::LOOK :BAD)) (RAISE "Can't look up the formals for ~x0!" CUTIL::FN)) ((UNLESS (SYMBOL-LISTP CUTIL::LOOK)) (RAISE "Expected a symbol-listp, but found ~x0!" CUTIL::LOOK))) CUTIL::LOOK)) (LOCAL (IN-THEORY (ENABLE CUTIL::LOOK-UP-FORMALS))) (DEFTHM CUTIL::SYMBOL-LISTP-OF-LOOK-UP-FORMALS (SYMBOL-LISTP (CUTIL::LOOK-UP-FORMALS CUTIL::FN WORLD))) (RECORD-EXPANSION (LOCAL (PROGN (ASSERT! (EQUAL (CUTIL::LOOK-UP-FORMALS (QUOTE CUTIL::LOOK-UP-FORMALS) (W STATE)) (QUOTE (CUTIL::FN WORLD)))))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE CUTIL::LOOK-UP-FORMALS)) (XDOC::PARENTS (QUOTE (CUTIL::SUPPORT))) (XDOC::SHORT (QUOTE "@(call look-up-formals) looks up the names of the arguments of the
function @('fn'), or causes a hard error if @('fn') isn't a function.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::LOOK-UP-FORMALS))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::LOOK-UP-FORMALS) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::SUPPORT) (:SHORT . "@(call look-up-formals) looks up the names of the arguments of the
function @('fn'), or causes a hard error if @('fn') isn't a function.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |CUTIL|::|LOOK-UP-FORMALS|)
@(def |CUTIL|::|SYMBOL-LISTP-OF-LOOK-UP-FORMALS|)") (:FROM . "[books]/cutil/look-up.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::LOOK-UP-FORMALS)))))) (VALUE-TRIPLE (QUOTE CUTIL::LOOK-UP-FORMALS))))) (6 RECORD-EXPANSION (DEFSECTION CUTIL::LOOK-UP-GUARD :PARENTS (CUTIL::SUPPORT) :SHORT "@(call look-up-guard) looks up the guard of the function @('fn'), or
causes a hard error if @('fn') isn't a function." (DEFUND CUTIL::LOOK-UP-GUARD (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((CUTIL::?TMP (CUTIL::LOOK-UP-FORMALS CUTIL::FN WORLD))) (GETPROP CUTIL::FN (QUOTE GUARD) T (QUOTE CURRENT-ACL2-WORLD) WORLD))) (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) CUTIL::X) (DEFUN CUTIL::F2 (CUTIL::X) (DECLARE (XARGS :GUARD (NATP CUTIL::X))) CUTIL::X) (DEFUN CUTIL::F3 (CUTIL::X) (DECLARE (XARGS :GUARD (AND (INTEGERP CUTIL::X) (<= 3 CUTIL::X) (<= CUTIL::X 13)))) CUTIL::X) (ASSERT! (EQUAL (CUTIL::LOOK-UP-GUARD (QUOTE CUTIL::F1) (W STATE)) (QUOTE T))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-GUARD (QUOTE CUTIL::F2) (W STATE)) (QUOTE (NATP CUTIL::X)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-GUARD (QUOTE CUTIL::F3) (W STATE)) (QUOTE (IF (INTEGERP CUTIL::X) (IF (NOT (< CUTIL::X (QUOTE 3))) (NOT (< (QUOTE 13) CUTIL::X)) (QUOTE NIL)) (QUOTE NIL)))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::LOOK-UP-GUARD)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::LOOK-UP-GUARD (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((CUTIL::?TMP (CUTIL::LOOK-UP-FORMALS CUTIL::FN WORLD))) (GETPROP CUTIL::FN (QUOTE GUARD) T (QUOTE CURRENT-ACL2-WORLD) WORLD))) (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) CUTIL::X) (DEFUN CUTIL::F2 (CUTIL::X) (DECLARE (XARGS :GUARD (NATP CUTIL::X))) CUTIL::X) (DEFUN CUTIL::F3 (CUTIL::X) (DECLARE (XARGS :GUARD (AND (INTEGERP CUTIL::X) (<= 3 CUTIL::X) (<= CUTIL::X 13)))) CUTIL::X) (ASSERT! (EQUAL (CUTIL::LOOK-UP-GUARD (QUOTE CUTIL::F1) (W STATE)) (QUOTE T))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-GUARD (QUOTE CUTIL::F2) (W STATE)) (QUOTE (NATP CUTIL::X)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-GUARD (QUOTE CUTIL::F3) (W STATE)) (QUOTE (IF (INTEGERP CUTIL::X) (IF (NOT (< CUTIL::X (QUOTE 3))) (NOT (< (QUOTE 13) CUTIL::X)) (QUOTE NIL)) (QUOTE NIL))))))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::LOOK-UP-GUARD (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((CUTIL::?TMP (CUTIL::LOOK-UP-FORMALS CUTIL::FN WORLD))) (GETPROP CUTIL::FN (QUOTE GUARD) T (QUOTE CURRENT-ACL2-WORLD) WORLD))) (RECORD-EXPANSION (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) CUTIL::X) (DEFUN CUTIL::F2 (CUTIL::X) (DECLARE (XARGS :GUARD (NATP CUTIL::X))) CUTIL::X) (DEFUN CUTIL::F3 (CUTIL::X) (DECLARE (XARGS :GUARD (AND (INTEGERP CUTIL::X) (<= 3 CUTIL::X) (<= CUTIL::X 13)))) CUTIL::X) (ASSERT! (EQUAL (CUTIL::LOOK-UP-GUARD (QUOTE CUTIL::F1) (W STATE)) (QUOTE T))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-GUARD (QUOTE CUTIL::F2) (W STATE)) (QUOTE (NATP CUTIL::X)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-GUARD (QUOTE CUTIL::F3) (W STATE)) (QUOTE (IF (INTEGERP CUTIL::X) (IF (NOT (< CUTIL::X (QUOTE 3))) (NOT (< (QUOTE 13) CUTIL::X)) (QUOTE NIL)) (QUOTE NIL))))))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE CUTIL::LOOK-UP-GUARD)) (XDOC::PARENTS (QUOTE (CUTIL::SUPPORT))) (XDOC::SHORT (QUOTE "@(call look-up-guard) looks up the guard of the function @('fn'), or
causes a hard error if @('fn') isn't a function.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::LOOK-UP-GUARD))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::LOOK-UP-GUARD) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::SUPPORT) (:SHORT . "@(call look-up-guard) looks up the guard of the function @('fn'), or
causes a hard error if @('fn') isn't a function.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |CUTIL|::|LOOK-UP-GUARD|)") (:FROM . "[books]/cutil/look-up.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::LOOK-UP-GUARD)))))) (VALUE-TRIPLE (QUOTE CUTIL::LOOK-UP-GUARD))))) (7 RECORD-EXPANSION (DEFSECTION CUTIL::LOOK-UP-RETURN-VALS :PARENTS (CUTIL::SUPPORT) :SHORT "@(call look-up-return-vals) returns the @('stobjs-out') property for
@('fn').  This is a list that may contain @('nil')s and @(see acl2::stobj) names,
with the same length as the number of return vals for @('fn')." (DEFUND CUTIL::LOOK-UP-RETURN-VALS (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOOK-UP-RETURN-VALS)) (CUTIL::STOBJS-OUT (GETPROP CUTIL::FN (QUOTE STOBJS-OUT) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((WHEN (EQ CUTIL::STOBJS-OUT :BAD)) (RAISE "Can't look up stobjs-out for ~x0!" CUTIL::FN) (QUOTE (NIL))) ((UNLESS (AND (CONSP CUTIL::STOBJS-OUT) (SYMBOL-LISTP CUTIL::STOBJS-OUT))) (RAISE "Expected stobjs-out to be a non-empty symbol-list, but ~
                  found ~x0." CUTIL::STOBJS-OUT) (QUOTE (NIL)))) CUTIL::STOBJS-OUT)) (LOCAL (IN-THEORY (ENABLE CUTIL::LOOK-UP-RETURN-VALS))) (DEFTHM CUTIL::SYMBOL-LISTP-OF-LOOK-UP-RETURN-VALS (SYMBOL-LISTP (CUTIL::LOOK-UP-RETURN-VALS CUTIL::FN WORLD))) (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) CUTIL::X) (DEFUN CUTIL::F2 (CUTIL::X) (MV CUTIL::X CUTIL::X)) (DEFUN CUTIL::F3 (CUTIL::X STATE) (DECLARE (XARGS :STOBJS STATE)) (MV CUTIL::X STATE)) (ASSERT! (EQUAL (CUTIL::LOOK-UP-RETURN-VALS (QUOTE CUTIL::F1) (W STATE)) (QUOTE (NIL)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-RETURN-VALS (QUOTE CUTIL::F2) (W STATE)) (QUOTE (NIL NIL)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-RETURN-VALS (QUOTE CUTIL::F3) (W STATE)) (QUOTE (NIL STATE))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::LOOK-UP-RETURN-VALS)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::LOOK-UP-RETURN-VALS (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOOK-UP-RETURN-VALS)) (CUTIL::STOBJS-OUT (GETPROP CUTIL::FN (QUOTE STOBJS-OUT) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((WHEN (EQ CUTIL::STOBJS-OUT :BAD)) (RAISE "Can't look up stobjs-out for ~x0!" CUTIL::FN) (QUOTE (NIL))) ((UNLESS (AND (CONSP CUTIL::STOBJS-OUT) (SYMBOL-LISTP CUTIL::STOBJS-OUT))) (RAISE "Expected stobjs-out to be a non-empty symbol-list, but ~
                  found ~x0." CUTIL::STOBJS-OUT) (QUOTE (NIL)))) CUTIL::STOBJS-OUT)) (LOCAL (IN-THEORY (ENABLE CUTIL::LOOK-UP-RETURN-VALS))) (DEFTHM CUTIL::SYMBOL-LISTP-OF-LOOK-UP-RETURN-VALS (SYMBOL-LISTP (CUTIL::LOOK-UP-RETURN-VALS CUTIL::FN WORLD))) (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) CUTIL::X) (DEFUN CUTIL::F2 (CUTIL::X) (MV CUTIL::X CUTIL::X)) (DEFUN CUTIL::F3 (CUTIL::X STATE) (DECLARE (XARGS :STOBJS STATE)) (MV CUTIL::X STATE)) (ASSERT! (EQUAL (CUTIL::LOOK-UP-RETURN-VALS (QUOTE CUTIL::F1) (W STATE)) (QUOTE (NIL)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-RETURN-VALS (QUOTE CUTIL::F2) (W STATE)) (QUOTE (NIL NIL)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-RETURN-VALS (QUOTE CUTIL::F3) (W STATE)) (QUOTE (NIL STATE)))))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::LOOK-UP-RETURN-VALS (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOOK-UP-RETURN-VALS)) (CUTIL::STOBJS-OUT (GETPROP CUTIL::FN (QUOTE STOBJS-OUT) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((WHEN (EQ CUTIL::STOBJS-OUT :BAD)) (RAISE "Can't look up stobjs-out for ~x0!" CUTIL::FN) (QUOTE (NIL))) ((UNLESS (AND (CONSP CUTIL::STOBJS-OUT) (SYMBOL-LISTP CUTIL::STOBJS-OUT))) (RAISE "Expected stobjs-out to be a non-empty symbol-list, but ~
                  found ~x0." CUTIL::STOBJS-OUT) (QUOTE (NIL)))) CUTIL::STOBJS-OUT)) (LOCAL (IN-THEORY (ENABLE CUTIL::LOOK-UP-RETURN-VALS))) (DEFTHM CUTIL::SYMBOL-LISTP-OF-LOOK-UP-RETURN-VALS (SYMBOL-LISTP (CUTIL::LOOK-UP-RETURN-VALS CUTIL::FN WORLD))) (RECORD-EXPANSION (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) CUTIL::X) (DEFUN CUTIL::F2 (CUTIL::X) (MV CUTIL::X CUTIL::X)) (DEFUN CUTIL::F3 (CUTIL::X STATE) (DECLARE (XARGS :STOBJS STATE)) (MV CUTIL::X STATE)) (ASSERT! (EQUAL (CUTIL::LOOK-UP-RETURN-VALS (QUOTE CUTIL::F1) (W STATE)) (QUOTE (NIL)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-RETURN-VALS (QUOTE CUTIL::F2) (W STATE)) (QUOTE (NIL NIL)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-RETURN-VALS (QUOTE CUTIL::F3) (W STATE)) (QUOTE (NIL STATE)))))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE CUTIL::LOOK-UP-RETURN-VALS)) (XDOC::PARENTS (QUOTE (CUTIL::SUPPORT))) (XDOC::SHORT (QUOTE "@(call look-up-return-vals) returns the @('stobjs-out') property for
@('fn').  This is a list that may contain @('nil')s and @(see acl2::stobj) names,
with the same length as the number of return vals for @('fn').")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::LOOK-UP-RETURN-VALS))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::LOOK-UP-RETURN-VALS) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::SUPPORT) (:SHORT . "@(call look-up-return-vals) returns the @('stobjs-out') property for
@('fn').  This is a list that may contain @('nil')s and @(see acl2::stobj) names,
with the same length as the number of return vals for @('fn').") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |CUTIL|::|LOOK-UP-RETURN-VALS|)
@(def |CUTIL|::|SYMBOL-LISTP-OF-LOOK-UP-RETURN-VALS|)") (:FROM . "[books]/cutil/look-up.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::LOOK-UP-RETURN-VALS)))))) (VALUE-TRIPLE (QUOTE CUTIL::LOOK-UP-RETURN-VALS))))) (8 RECORD-EXPANSION (DEFSECTION CUTIL::LOOK-UP-WRAPPER-ARGS :PARENTS (CUTIL::SUPPORT) :SHORT "@(call look-up-wrapper-args) is like @(see look-up-formals), except
that @('wrapper') can be either a function or a macro, and in the macro case
the arguments we return may include lambda-list keywords; see @(see
macro-args)." (DEFUND CUTIL::LOOK-UP-WRAPPER-ARGS (CUTIL::WRAPPER WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::WRAPPER) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOOK-UP-WRAPPER-ARGS)) (CUTIL::LOOK (GETPROP CUTIL::WRAPPER (QUOTE FORMALS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((UNLESS (EQ CUTIL::LOOK :BAD)) CUTIL::LOOK) (CUTIL::LOOK (GETPROP CUTIL::WRAPPER (QUOTE MACRO-ARGS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((UNLESS (EQ CUTIL::LOOK :BAD)) CUTIL::LOOK)) (RAISE "Failed to find formals or macro-args for ~x0!" CUTIL::WRAPPER))) (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) CUTIL::X) (DEFMACRO CUTIL::F2 (CUTIL::X) CUTIL::X) (DEFMACRO CUTIL::F3 (CUTIL::X CUTIL::Y &KEY (CUTIL::C (QUOTE 5)) (CUTIL::D (QUOTE 7))) (LIST CUTIL::X CUTIL::Y CUTIL::C CUTIL::D)) (ASSERT! (EQUAL (CUTIL::LOOK-UP-WRAPPER-ARGS (QUOTE CUTIL::F1) (W STATE)) (QUOTE (CUTIL::X)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-WRAPPER-ARGS (QUOTE CUTIL::F2) (W STATE)) (QUOTE (CUTIL::X)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-WRAPPER-ARGS (QUOTE CUTIL::F3) (W STATE)) (QUOTE (CUTIL::X CUTIL::Y &KEY (CUTIL::C (QUOTE 5)) (CUTIL::D (QUOTE 7))))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::LOOK-UP-WRAPPER-ARGS)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::LOOK-UP-WRAPPER-ARGS (CUTIL::WRAPPER WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::WRAPPER) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOOK-UP-WRAPPER-ARGS)) (CUTIL::LOOK (GETPROP CUTIL::WRAPPER (QUOTE FORMALS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((UNLESS (EQ CUTIL::LOOK :BAD)) CUTIL::LOOK) (CUTIL::LOOK (GETPROP CUTIL::WRAPPER (QUOTE MACRO-ARGS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((UNLESS (EQ CUTIL::LOOK :BAD)) CUTIL::LOOK)) (RAISE "Failed to find formals or macro-args for ~x0!" CUTIL::WRAPPER))) (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) CUTIL::X) (DEFMACRO CUTIL::F2 (CUTIL::X) CUTIL::X) (DEFMACRO CUTIL::F3 (CUTIL::X CUTIL::Y &KEY (CUTIL::C (QUOTE 5)) (CUTIL::D (QUOTE 7))) (LIST CUTIL::X CUTIL::Y CUTIL::C CUTIL::D)) (ASSERT! (EQUAL (CUTIL::LOOK-UP-WRAPPER-ARGS (QUOTE CUTIL::F1) (W STATE)) (QUOTE (CUTIL::X)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-WRAPPER-ARGS (QUOTE CUTIL::F2) (W STATE)) (QUOTE (CUTIL::X)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-WRAPPER-ARGS (QUOTE CUTIL::F3) (W STATE)) (QUOTE (CUTIL::X CUTIL::Y &KEY (CUTIL::C (QUOTE 5)) (CUTIL::D (QUOTE 7)))))))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::LOOK-UP-WRAPPER-ARGS (CUTIL::WRAPPER WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::WRAPPER) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOOK-UP-WRAPPER-ARGS)) (CUTIL::LOOK (GETPROP CUTIL::WRAPPER (QUOTE FORMALS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((UNLESS (EQ CUTIL::LOOK :BAD)) CUTIL::LOOK) (CUTIL::LOOK (GETPROP CUTIL::WRAPPER (QUOTE MACRO-ARGS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((UNLESS (EQ CUTIL::LOOK :BAD)) CUTIL::LOOK)) (RAISE "Failed to find formals or macro-args for ~x0!" CUTIL::WRAPPER))) (RECORD-EXPANSION (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) CUTIL::X) (DEFMACRO CUTIL::F2 (CUTIL::X) CUTIL::X) (DEFMACRO CUTIL::F3 (CUTIL::X CUTIL::Y &KEY (CUTIL::C (QUOTE 5)) (CUTIL::D (QUOTE 7))) (LIST CUTIL::X CUTIL::Y CUTIL::C CUTIL::D)) (ASSERT! (EQUAL (CUTIL::LOOK-UP-WRAPPER-ARGS (QUOTE CUTIL::F1) (W STATE)) (QUOTE (CUTIL::X)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-WRAPPER-ARGS (QUOTE CUTIL::F2) (W STATE)) (QUOTE (CUTIL::X)))) (ASSERT! (EQUAL (CUTIL::LOOK-UP-WRAPPER-ARGS (QUOTE CUTIL::F3) (W STATE)) (QUOTE (CUTIL::X CUTIL::Y &KEY (CUTIL::C (QUOTE 5)) (CUTIL::D (QUOTE 7)))))))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE CUTIL::LOOK-UP-WRAPPER-ARGS)) (XDOC::PARENTS (QUOTE (CUTIL::SUPPORT))) (XDOC::SHORT (QUOTE "@(call look-up-wrapper-args) is like @(see look-up-formals), except
that @('wrapper') can be either a function or a macro, and in the macro case
the arguments we return may include lambda-list keywords; see @(see
macro-args).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::LOOK-UP-WRAPPER-ARGS))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::LOOK-UP-WRAPPER-ARGS) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::SUPPORT) (:SHORT . "@(call look-up-wrapper-args) is like @(see look-up-formals), except
that @('wrapper') can be either a function or a macro, and in the macro case
the arguments we return may include lambda-list keywords; see @(see
macro-args).") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |CUTIL|::|LOOK-UP-WRAPPER-ARGS|)") (:FROM . "[books]/cutil/look-up.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::LOOK-UP-WRAPPER-ARGS)))))) (VALUE-TRIPLE (QUOTE CUTIL::LOOK-UP-WRAPPER-ARGS))))) (9 RECORD-EXPANSION (DEFSECTION CUTIL::LOGIC-MODE-P :PARENTS (CUTIL::SUPPORT) :SHORT "@(call logic-mode-p) looks up the function @('fn') and returns
@('t') if @('fn') is in logic mode, or @('nil') otherwise.  It causes a
hard error if @('fn') isn't a function." (DEFUND CUTIL::LOGIC-MODE-P (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOGIC-MODE-P)) (CUTIL::LOOK (GETPROP CUTIL::FN (QUOTE FORMALS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((WHEN (EQ CUTIL::LOOK :BAD)) (RAISE "Can't look up the formals for ~x0!" CUTIL::FN)) (CUTIL::SYMBOL-CLASS (GETPROP CUTIL::FN (QUOTE SYMBOL-CLASS) NIL (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((UNLESS (MEMBER CUTIL::SYMBOL-CLASS (QUOTE (:COMMON-LISP-COMPLIANT :IDEAL :PROGRAM)))) (RAISE "Unexpected symbol-class for ~x0: ~x1." CUTIL::FN CUTIL::SYMBOL-CLASS))) (NOT (EQ CUTIL::SYMBOL-CLASS :PROGRAM)))) (LOCAL (IN-THEORY (ENABLE CUTIL::LOGIC-MODE-P))) (DEFTHM CUTIL::BOOLEANP-OF-LOOK-UP-FORMALS (OR (EQUAL (CUTIL::LOGIC-MODE-P CUTIL::FN WORLD) T) (EQUAL (CUTIL::LOGIC-MODE-P CUTIL::FN WORLD) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (PROGN (DEFUN CUTIL::F (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM)) CUTIL::X) (DEFUN CUTIL::G (CUTIL::X) CUTIL::X) (DEFUN CUTIL::H (CUTIL::X) (DECLARE (XARGS :VERIFY-GUARDS T)) CUTIL::X) (ASSERT! (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::G) (W STATE))) (ASSERT! (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::H) (W STATE))) (ASSERT! (NOT (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::F) (W STATE))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::LOGIC-MODE-P)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::LOGIC-MODE-P (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOGIC-MODE-P)) (CUTIL::LOOK (GETPROP CUTIL::FN (QUOTE FORMALS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((WHEN (EQ CUTIL::LOOK :BAD)) (RAISE "Can't look up the formals for ~x0!" CUTIL::FN)) (CUTIL::SYMBOL-CLASS (GETPROP CUTIL::FN (QUOTE SYMBOL-CLASS) NIL (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((UNLESS (MEMBER CUTIL::SYMBOL-CLASS (QUOTE (:COMMON-LISP-COMPLIANT :IDEAL :PROGRAM)))) (RAISE "Unexpected symbol-class for ~x0: ~x1." CUTIL::FN CUTIL::SYMBOL-CLASS))) (NOT (EQ CUTIL::SYMBOL-CLASS :PROGRAM)))) (LOCAL (IN-THEORY (ENABLE CUTIL::LOGIC-MODE-P))) (DEFTHM CUTIL::BOOLEANP-OF-LOOK-UP-FORMALS (OR (EQUAL (CUTIL::LOGIC-MODE-P CUTIL::FN WORLD) T) (EQUAL (CUTIL::LOGIC-MODE-P CUTIL::FN WORLD) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (PROGN (DEFUN CUTIL::F (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM)) CUTIL::X) (DEFUN CUTIL::G (CUTIL::X) CUTIL::X) (DEFUN CUTIL::H (CUTIL::X) (DECLARE (XARGS :VERIFY-GUARDS T)) CUTIL::X) (ASSERT! (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::G) (W STATE))) (ASSERT! (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::H) (W STATE))) (ASSERT! (NOT (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::F) (W STATE)))))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::LOGIC-MODE-P (CUTIL::FN WORLD) (DECLARE (XARGS :GUARD (AND (SYMBOLP CUTIL::FN) (PLIST-WORLDP WORLD)))) (B* ((__FUNCTION__ (QUOTE CUTIL::LOGIC-MODE-P)) (CUTIL::LOOK (GETPROP CUTIL::FN (QUOTE FORMALS) :BAD (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((WHEN (EQ CUTIL::LOOK :BAD)) (RAISE "Can't look up the formals for ~x0!" CUTIL::FN)) (CUTIL::SYMBOL-CLASS (GETPROP CUTIL::FN (QUOTE SYMBOL-CLASS) NIL (QUOTE CURRENT-ACL2-WORLD) WORLD)) ((UNLESS (MEMBER CUTIL::SYMBOL-CLASS (QUOTE (:COMMON-LISP-COMPLIANT :IDEAL :PROGRAM)))) (RAISE "Unexpected symbol-class for ~x0: ~x1." CUTIL::FN CUTIL::SYMBOL-CLASS))) (NOT (EQ CUTIL::SYMBOL-CLASS :PROGRAM)))) (LOCAL (IN-THEORY (ENABLE CUTIL::LOGIC-MODE-P))) (DEFTHM CUTIL::BOOLEANP-OF-LOOK-UP-FORMALS (OR (EQUAL (CUTIL::LOGIC-MODE-P CUTIL::FN WORLD) T) (EQUAL (CUTIL::LOGIC-MODE-P CUTIL::FN WORLD) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION) (RECORD-EXPANSION (LOCAL (PROGN (DEFUN CUTIL::F (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM)) CUTIL::X) (DEFUN CUTIL::G (CUTIL::X) CUTIL::X) (DEFUN CUTIL::H (CUTIL::X) (DECLARE (XARGS :VERIFY-GUARDS T)) CUTIL::X) (ASSERT! (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::G) (W STATE))) (ASSERT! (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::H) (W STATE))) (ASSERT! (NOT (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::F) (W STATE)))))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE CUTIL::LOGIC-MODE-P)) (XDOC::PARENTS (QUOTE (CUTIL::SUPPORT))) (XDOC::SHORT (QUOTE "@(call logic-mode-p) looks up the function @('fn') and returns
@('t') if @('fn') is in logic mode, or @('nil') otherwise.  It causes a
hard error if @('fn') isn't a function.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::LOGIC-MODE-P))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::LOGIC-MODE-P) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::SUPPORT) (:SHORT . "@(call logic-mode-p) looks up the function @('fn') and returns
@('t') if @('fn') is in logic mode, or @('nil') otherwise.  It causes a
hard error if @('fn') isn't a function.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |CUTIL|::|LOGIC-MODE-P|)
@(def |CUTIL|::|BOOLEANP-OF-LOOK-UP-FORMALS|)") (:FROM . "[books]/cutil/look-up.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::LOGIC-MODE-P)))))) (VALUE-TRIPLE (QUOTE CUTIL::LOGIC-MODE-P))))))
(("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
(("/usr/share/acl2-6.3/books/cutil/look-up.lisp" "look-up" "look-up" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1505505915) (LOCAL ("/usr/share/acl2-6.3/books/misc/assert.lisp" "misc/assert" "assert" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1184956729)) (LOCAL ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718)) ("/usr/share/acl2-6.3/books/cutil/support.lisp" "support" "support" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1180314020) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "tools/bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439) ("/usr/share/acl2-6.3/books/misc/definline.lisp" "misc/definline" "definline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1571016648) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
1143962636
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / cutil / look-up.cert
