~$ acl2 Welcome to Clozure Common Lisp Version 1.12-dev/v1.12-dev.1-3-g1944cfb (DarwinX8664)! ACL2 Version 8.0 built April 28, 2018 12:06:49. Copyright (C) 2017, Regents of the University of Texas ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the LICENSE file distributed with ACL2. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + WARNING: This is NOT an ACL2 release; it is a development snapshot + + (git commit hash: 3e92fab85f66ca73f7b225bc84e77d5317340c10). + + On rare occasions development snapshots may be incomplete, fragile, + + or unable to pass the usual regression tests. + +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-8-0 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 8.0. Level 1. Cbd "/Users/kaufmann/". System books directory "/Users/kaufmann/acl2/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(list 'defun 'f1 '(x) '(cons x x)) (DEFUN F1 (X) (CONS X X)) ACL2 !>(list 'defun 'f1 '(x) '(cons x x)) (DEFUN F1 (X) (CONS X X)) ACL2 !>'(defun f1 (x) (cons x x)) ; same result as above (DEFUN F1 (X) (CONS X X)) ACL2 !>(let ((y 'x)) `(defun f1 (,y) (cons ,y ,y))) ; same result as above (DEFUN F1 (X) (CONS X X)) ACL2 !>(make-event (list 'defun 'f1 '(x) '(cons x x))) Since F1 is non-recursive, its admission is trivial. We observe that the type of F1 is described by the theorem (CONSP (F1 X)). We used primitive type reasoning. Summary Form: ( DEFUN F1 ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) Summary Form: ( MAKE-EVENT (LIST ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) F1 ACL2 !>:pe f1 L 1:x(MAKE-EVENT (LIST # # ...)) \ >L (DEFUN F1 (X) (CONS X X)) ACL2 !>:pf f1 (EQUAL (F1 X) (CONS X X)) ACL2 !>(length (w state)) 110327 ACL2 !>(value-triple (length (w state))) 110327 ACL2 !>(length (w state))' 110327 ACL2 !>3 3 ACL2 !>(list 'defconst '*world-length* (length (w state))) (DEFCONST *WORLD-LENGTH* 110327) ACL2 !>(make-event (list 'defconst '*world-length* (length (w state)))) Summary Form: ( DEFCONST *WORLD-LENGTH* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Summary Form: ( MAKE-EVENT (LIST ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) *WORLD-LENGTH* ACL2 !>*world-length* 110327 ACL2 !>(cw "~x0~%" *world-length*) 110327 NIL ACL2 !>(fmt-cw "~x0~%" *world-length*) ACL2 Error in TOP-LEVEL: The symbol FMT-CW (in package "ACL2") has neither a function nor macro definition in ACL2. Please define it. See :DOC near-misses. Note: this error occurred in the context (FMT-CW "~x0~%" *WORLD-LENGTH*). ACL2 !>:pe *world-length* 2:x(MAKE-EVENT (LIST # # ...)) \ > (DEFCONST *WORLD-LENGTH* 110327) ACL2 !>(defmacro define-world-length-constant (name) `(make-event (list 'defconst ',name (length (w state))))) Summary Form: ( DEFMACRO DEFINE-WORLD-LENGTH-CONSTANT ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DEFINE-WORLD-LENGTH-CONSTANT ACL2 !>:trans1 (define-world-length-constant *new-wl*) (MAKE-EVENT (LIST 'DEFCONST '*NEW-WL* (LENGTH (W STATE)))) ACL2 !>(define-world-length-constant *new-wl*) Summary Form: ( DEFCONST *NEW-WL* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Summary Form: ( MAKE-EVENT (LIST ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) *NEW-WL* ACL2 !>:pe *NEW-WL* 4:x(DEFINE-WORLD-LENGTH-CONSTANT *NEW-WL*) \ > (DEFCONST *NEW-WL* 110341) ACL2 !> (cw "~x0~%" *new-wl*) 110341 NIL ACL2 !>(cw "~x0~%" *new-wl*) 110341 NIL ACL2 !>(quote "A bit of background about error triples -- three faces of a simple example.") "A bit of background about error triples -- three faces of a simple example." ACL2 !>(mv nil 3) (NIL 3) ACL2 !>(mv nil 3 state) 3 ACL2 !>(mv t 3 state) ACL2 !>(mv nil 3 state 4) (NIL 3 4) ACL2 !>(defun h (x) x) Since H is non-recursive, its admission is trivial. We observe that the type of H is described by the theorem (EQUAL (H X) X). Summary Form: ( DEFUN H ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H ACL2 !>:u 4:x(DEFINE-WORLD-LENGTH-CONSTANT *NEW-WL*) ACL2 !>(mv nil 3 state) 3 ACL2 !>(mv nil (+ 3 4) state) 7 ACL2 !>(mv nil (make-list 100) state) (NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL) ACL2 !>(mv nil 3 state) 3 ACL2 !>(value 3) ; same as (mv nil 3 state) 3 ACL2 !>(value-triple 3) ; This one is an event. 3 ACL2 !>(progn (value-triple 3) (defun h (x) x)) ACL2 !>>(VALUE-TRIPLE 3) 3 ACL2 !>>(DEFUN H (X) X) Since H is non-recursive, its admission is trivial. We observe that the type of H is described by the theorem (EQUAL (H X) X). Summary Form: ( DEFUN H ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H Summary Form: ( PROGN (VALUE-TRIPLE 3 ...) ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H ACL2 !>:u 4:x(DEFINE-WORLD-LENGTH-CONSTANT *NEW-WL*) ACL2 !>(progn (value 3) (defun h (x) x)) ACL2 !>>(VALUE 3) ACL2 Error in ( PROGN (VALUE 3 ...) ...): The form (MV NIL 3 STATE) is not an embedded event form. See :DOC embedded-event-form. Note: the above form was encountered during processing of (VALUE 3). Calls of the macro MV do not generate an event, because this macro has special meaning that is not handled by ACL2's event-generation mechanism. Please contact the implementors if this seems to be a hardship. ACL2 Error in ( PROGN (VALUE 3 ...) ...): PROGN may only be used on legal event forms (see :DOC embedded-event-form). Consider using ER- PROGN instead. Summary Form: ( PROGN (VALUE 3 ...) ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( PROGN (VALUE 3 ...) ...): See :DOC failure. ******** FAILED ******** ACL2 !>(pbt 0) ; But value-triple events do not change the world. 0 (EXIT-BOOT-STRAP-MODE) L 1 (MAKE-EVENT (LIST # # ...)) 2 (MAKE-EVENT (LIST # # ...)) 3 (DEFMACRO DEFINE-WORLD-LENGTH-CONSTANT (NAME) ...) 4:x(DEFINE-WORLD-LENGTH-CONSTANT *NEW-WL*) ACL2 !>(value-triple 3) ; This one is an event. 3 ACL2 !>(pbt 0) ; But value-triple events do not change the world. 0 (EXIT-BOOT-STRAP-MODE) L 1 (MAKE-EVENT (LIST # # ...)) 2 (MAKE-EVENT (LIST # # ...)) 3 (DEFMACRO DEFINE-WORLD-LENGTH-CONSTANT (NAME) ...) 4:x(DEFINE-WORLD-LENGTH-CONSTANT *NEW-WL*) ACL2 !>(quote "Consider the popular macro define") "Consider the popular macro define" ACL2 !>(include-book "std/util/define" :dir :system) Summary Form: ( INCLUDE-BOOK "std/util/define" ...) Rules: NIL Time: 0.30 seconds (prove: 0.00, print: 0.00, other: 0.30) "/Users/kaufmann/acl2/acl2/books/std/util/define.lisp" ACL2 !>:trans1 (define foo (x) x) (WITH-OUTPUT :STACK :PUSH :ON (ERROR) :OFF :ALL (MAKE-EVENT (STD::DEFINE-FN 'FOO '((X) X) (W STATE)))) ACL2 !>(STD::DEFINE-FN 'FOO '((X) X) (W STATE)) (PROGN (DEFSECTION FOO (WITH-OUTPUT :STACK :POP (DEFUN FOO (X) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ 'FOO)) (DECLARE (IGNORABLE __FUNCTION__)) X))) (TABLE DEFINE 'STD::GUTS-ALIST (CONS (CONS 'FOO '((STD::NAME . FOO) (STD::NAME-FN . FOO) (STD::KWD-ALIST) (STD::RETURNSPECS) (STD::T-PROOF) (STD::MAIN-DEF DEFUN FOO (X) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ 'FOO)) (DECLARE (IGNORABLE __FUNCTION__)) X)) (STD::MACRO) (STD::RAW-FORMALS X) (STD::FORMALS (:FORMAL (STD::NAME . X) (GUARD . T) (DOC . "") (STD::OPTS))) (STD::REST-EVENTS) (STD::PE-ENTRY DEFINE FOO (X) X))) (STD::GET-DEFINE-GUTS-ALIST WORLD))) (STD::SET-DEFINE-CURRENT-FUNCTION FOO) (LOCAL (MAKE-EVENT (IF (STD::LOGIC-MODE-P 'FOO (W STATE)) '(IN-THEORY (ENABLE FOO)) '(VALUE-TRIPLE :INVISIBLE)))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (STD::EVENTS (STD::RETURNSPEC-THMS 'FOO 'FOO 'NIL WORLD))) (VALUE (IF STD::EVENTS (CONS 'WITH-OUTPUT (CONS ':STACK (CONS ':POP (CONS (CONS 'PROGN STD::EVENTS) 'NIL)))) '(VALUE-TRIPLE :INVISIBLE))))) (EXTEND-PE-TABLE FOO (DEFINE FOO (X) X)) (MAKE-EVENT (IF (STD::LOGIC-MODE-P 'FOO (W STATE)) '(IN-THEORY (DISABLE FOO)) '(VALUE-TRIPLE :INVISIBLE)))) (MAKE-EVENT (B* ((STD::CURRENT-PKG (F-GET-GLOBAL 'CURRENT-PACKAGE STATE)) (STD::BASE-PKG (PKG-WITNESS STD::CURRENT-PKG)) (STD::NAME 'FOO) (STD::ALL-TOPICS (XDOC::GET-XDOC-TABLE (W STATE))) (STD::OLD-TOPIC (XDOC::FIND-TOPIC STD::NAME STD::ALL-TOPICS)) ((UNLESS STD::OLD-TOPIC) (VALUE '(VALUE-TRIPLE :INVISIBLE))) ((MV STD::STR STATE) (STD::MAKE-XDOC-TOP STD::NAME 'FOO '((:FORMAL (STD::NAME . X) (GUARD . T) (DOC . "") (STD::OPTS))) 'NIL STD::BASE-PKG STATE)) (EVENT (LIST 'XDOC::XDOC-PREPEND STD::NAME STD::STR))) (VALUE EVENT))) (MAKE-EVENT (LIST 'VALUE-TRIPLE (IF (EQL 9445 (MAX-ABSOLUTE-EVENT-NUMBER (W STATE))) :REDUNDANT ''FOO)))) ACL2 !>(PROGN (DEFUN FOO (X Y) (CONS Y X)) (VALUE-TRIPLE (LIST 'VALUE-TRIPLE (LIST 'QUOTE (FOO 3 4))))) ACL2 !>>(DEFUN FOO (X Y) (CONS Y X)) Since FOO is non-recursive, its admission is trivial. We observe that the type of FOO is described by the theorem (CONSP (FOO X Y)). We used primitive type reasoning. Summary Form: ( DEFUN FOO ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>>(VALUE-TRIPLE (LIST 'VALUE-TRIPLE (LIST 'QUOTE (FOO 3 4)))) (VALUE-TRIPLE '(4 . 3)) Summary Form: ( PROGN (DEFUN FOO ...) ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) (VALUE-TRIPLE '(4 . 3)) ; (value-triple (quote (4 . 3))) ACL2 !>(VALUE-TRIPLE '(4 . 3)) (4 . 3) ACL2 !>(u) ; undo the progn d 5:x(INCLUDE-BOOK "std/util/define" :DIR ...) ACL2 !>(defun run-def-form (def expr) ; The expansion phase of the make-event below will evaluate the given ; definition and then return the form (value-triple val), where val is the ; value of expr. `(make-event (progn ,def (value-triple (list 'value-triple (list 'quote ,expr)))))) Since RUN-DEF-FORM is non-recursive, its admission is trivial. We observe that the type of RUN-DEF-FORM is described by the theorem (AND (CONSP (RUN-DEF-FORM DEF EXPR)) (TRUE-LISTP (RUN-DEF-FORM DEF EXPR))). We used primitive type reasoning. Summary Form: ( DEFUN RUN-DEF-FORM ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) RUN-DEF-FORM ACL2 !>(run-def-form '(DEFUN FOO (X Y) (CONS Y X)) '(FOO 3 4)) (MAKE-EVENT (PROGN (DEFUN FOO (X Y) (CONS Y X)) (VALUE-TRIPLE (LIST 'VALUE-TRIPLE (LIST 'QUOTE (FOO 3 4)))))) ACL2 !>(PROGN (DEFUN FOO (X Y) (CONS Y X)) (VALUE-TRIPLE (LIST 'VALUE-TRIPLE (LIST 'QUOTE (FOO 3 4))))) ACL2 !>>(DEFUN FOO (X Y) (CONS Y X)) Since FOO is non-recursive, its admission is trivial. We observe that the type of FOO is described by the theorem (CONSP (FOO X Y)). We used primitive type reasoning. Summary Form: ( DEFUN FOO ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>>(VALUE-TRIPLE (LIST 'VALUE-TRIPLE (LIST 'QUOTE (FOO 3 4)))) (VALUE-TRIPLE '(4 . 3)) Summary Form: ( PROGN (DEFUN FOO ...) ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) (VALUE-TRIPLE '(4 . 3)) ACL2 !>(pe 'foo) L 7:x(PROGN (DEFUN FOO # ...) (VALUE-TRIPLE #)) \ >L (DEFUN FOO (X Y) (CONS Y X)) ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (MAKE-EVENT (LIST # # ...)) 2 (MAKE-EVENT (LIST # # ...)) 3 (DEFMACRO DEFINE-WORLD-LENGTH-CONSTANT (NAME) ...) 4 (DEFINE-WORLD-LENGTH-CONSTANT *NEW-WL*) d 5 (INCLUDE-BOOK "std/util/define" :DIR ...) L 6 (DEFUN RUN-DEF-FORM (DEF EXPR) ...) L 7:x(PROGN (DEFUN FOO # ...) (VALUE-TRIPLE #)) ACL2 !>(u) L 6:x(DEFUN RUN-DEF-FORM (DEF EXPR) ...) ACL2 !>(with-output :off :all (MAKE-EVENT (PROGN (DEFUN FOO (X Y) (CONS Y X)) (VALUE-TRIPLE (LIST 'VALUE-TRIPLE (LIST 'QUOTE (FOO 3 4))))))) (4 . 3) ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (MAKE-EVENT (LIST # # ...)) 2 (MAKE-EVENT (LIST # # ...)) 3 (DEFMACRO DEFINE-WORLD-LENGTH-CONSTANT (NAME) ...) 4 (DEFINE-WORLD-LENGTH-CONSTANT *NEW-WL*) d 5 (INCLUDE-BOOK "std/util/define" :DIR ...) L 6:x(DEFUN RUN-DEF-FORM (DEF EXPR) ...) ACL2 !>(VALUE-TRIPLE '(4 . 3)) (4 . 3) ACL2 !>(quote "Consider this call of run-def-form.") "Consider this call of run-def-form." ACL2 !>(run-def-form `(defun my-mem (lst) (declare (xargs :guard (true-listp lst))) (cond ((endp lst) nil) ((EQ (car lst) 'C) t) (t (my-mem (cdr lst))))) `(my-mem '(A B C D))) (MAKE-EVENT (PROGN (DEFUN MY-MEM (LST) (DECLARE (XARGS :GUARD (TRUE-LISTP LST))) (COND ((ENDP LST) NIL) ((EQ (CAR LST) 'C) T) (T (MY-MEM (CDR LST))))) (VALUE-TRIPLE (LIST 'VALUE-TRIPLE (LIST 'QUOTE (MY-MEM '(A B C D))))))) ACL2 !>(quote "Here it is again, more programmatically; I'll explain.") "Here it is again, more programmatically; I'll explain." ACL2 !>(let ((elt 'c) (x '(a b c d))) (let ((eq-fn (cond ((symbolp elt) 'eq) ((eqlablep elt) 'eql) (t 'equal)))) (run-def-form `(defun my-mem (lst) (declare (xargs :guard (true-listp lst))) (cond ((endp lst) nil) ((,eq-fn (car lst) ',elt) t) (t (my-mem (cdr lst))))) `(my-mem ',x)))) (MAKE-EVENT (PROGN (DEFUN MY-MEM (LST) (DECLARE (XARGS :GUARD (TRUE-LISTP LST))) (COND ((ENDP LST) NIL) ((EQ (CAR LST) 'C) T) (T (MY-MEM (CDR LST))))) (VALUE-TRIPLE (LIST 'VALUE-TRIPLE (LIST 'QUOTE (MY-MEM '(A B C D))))))) ACL2 !>(quote "And here we run a make-event form that evaluates the form above to get the make-event expansion.") "And here we run a make-event form that evaluates the form above to get the make-event expansion." ACL2 !>(defun search-list-fn (elt x) (declare (xargs :guard t)) `(with-output ; inhibit output :off :all ; all output is inhibited except: :on error ; allow error output (make-event (let ((elt ,elt) (x ,x)) (let ((eq-fn (cond ((symbolp elt) 'eq) ((eqlablep elt) 'eql) (t 'equal)))) (run-def-form `(defun my-mem (lst) (declare (xargs :guard (true-listp lst))) (cond ((endp lst) nil) ((,eq-fn (car lst) ',elt) t) (t (my-mem (cdr lst))))) `(my-mem ',x))))))) Since SEARCH-LIST-FN is non-recursive, its admission is trivial. We observe that the type of SEARCH-LIST-FN is described by the theorem (AND (CONSP (SEARCH-LIST-FN ELT X)) (TRUE-LISTP (SEARCH-LIST-FN ELT X))). We used primitive type reasoning. Computing the guard conjecture for SEARCH-LIST-FN.... The guard conjecture for SEARCH-LIST-FN is trivial to prove, given the :executable-counterpart of CONS. SEARCH-LIST-FN is compliant with Common Lisp. Summary Form: ( DEFUN SEARCH-LIST-FN ...) Rules: ((:EXECUTABLE-COUNTERPART CONS) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.03) SEARCH-LIST-FN ACL2 !>(quote "Write a macro that expands by calling the function above.") "Write a macro that expands by calling the function above." ACL2 !>(defmacro search-list (elt x) (search-list-fn elt x)) Summary Form: ( DEFMACRO SEARCH-LIST ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) SEARCH-LIST ACL2 !>(quote "Examples:") "Examples:" ACL2 !>(search-list 'a (append '(x y z) '(b c))) NIL ACL2 !>(search-list 'z (append '(x y z) '(b c))) T ACL2 !>(mv-let (erp val state) (search-list '(a b) '((c d) (a b))) (declare (ignore erp)) (value val)) T ACL2 !>(er-let* ((val (search-list '(a b) '((c d) (a b))))) (declare (ignore erp)) (value (if (eq val t) "HOORAY" "BOO"))) ACL2 Error in macro expansion: Wrong number of args in macro expansion of (ER-LET* ((VAL (SEARCH-LIST '# '#))) (DECLARE (IGNORE ERP)) (VALUE (IF (EQ VAL T) "HOORAY" "BOO"))). (See :DOC set-iprint to be able to see elided values in this message.) ACL2 !>(er-let* ((val (search-list '(a b) '((c d) (a b))))) (value (if (eq val t) "HOORAY" "BOO"))) "HOORAY" ACL2 !>(er-let* ((val (search-list '(a b x) '((c d) (a b))))) (value (if (eq val t) "HOORAY" "BOO"))) "BOO" ACL2 !>:trans1 (search-list '(a b) '((c d) (a b))) (WITH-OUTPUT :OFF :ALL :ON ERROR (MAKE-EVENT (LET ((ELT '(A B)) (X '((C D) (A B)))) (LET ((EQ-FN (COND ((SYMBOLP ELT) 'EQ) ((EQLABLEP ELT) 'EQL) (T 'EQUAL)))) (RUN-DEF-FORM (CONS 'DEFUN (CONS 'MY-MEM (CONS (CONS 'LST 'NIL) (CONS (CONS 'DECLARE (CONS (CONS 'XARGS (CONS ':GUARD (CONS (CONS 'TRUE-LISTP (CONS 'LST 'NIL)) 'NIL))) 'NIL)) (CONS (CONS 'COND (CONS (CONS (CONS 'ENDP (CONS 'LST 'NIL)) (CONS 'NIL 'NIL)) (CONS (CONS (CONS EQ-FN (CONS (CONS 'CAR (CONS 'LST 'NIL)) (CONS (CONS 'QUOTE (CONS ELT 'NIL)) 'NIL))) (CONS 'T 'NIL)) (CONS (CONS 'T (CONS (CONS 'MY-MEM (CONS (CONS 'CDR (CONS 'LST 'NIL)) 'NIL)) 'NIL)) 'NIL)))) 'NIL))))) (CONS 'MY-MEM (CONS (CONS 'QUOTE (CONS X 'NIL)) 'NIL))))))) ACL2 !>(LET ((ELT '(A B)) (X '((C D) (A B)))) (LET ((EQ-FN (COND ((SYMBOLP ELT) 'EQ) ((EQLABLEP ELT) 'EQL) (T 'EQUAL)))) (RUN-DEF-FORM (CONS 'DEFUN (CONS 'MY-MEM (CONS (CONS 'LST 'NIL) (CONS (CONS 'DECLARE (CONS (CONS 'XARGS (CONS ':GUARD (CONS (CONS 'TRUE-LISTP (CONS 'LST 'NIL)) 'NIL))) 'NIL)) (CONS (CONS 'COND (CONS (CONS (CONS 'ENDP (CONS 'LST 'NIL)) (CONS 'NIL 'NIL)) (CONS (CONS (CONS EQ-FN (CONS (CONS 'CAR (CONS 'LST 'NIL)) (CONS (CONS 'QUOTE (CONS ELT 'NIL)) 'NIL))) (CONS 'T 'NIL)) (CONS (CONS 'T (CONS (CONS 'MY-MEM (CONS (CONS 'CDR (CONS 'LST 'NIL)) 'NIL)) 'NIL)) 'NIL)))) 'NIL))))) (CONS 'MY-MEM (CONS (CONS 'QUOTE (CONS X 'NIL)) 'NIL))))) (MAKE-EVENT (PROGN (DEFUN MY-MEM (LST) (DECLARE (XARGS :GUARD (TRUE-LISTP LST))) (COND ((ENDP LST) NIL) ((EQUAL (CAR LST) '(A B)) T) (T (MY-MEM (CDR LST))))) (VALUE-TRIPLE (LIST 'VALUE-TRIPLE (LIST 'QUOTE (MY-MEM '((C D) (A B)))))))) ACL2 !>