Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Std/lists
Std/lists/abstract
Element-list-p
Element-list-equiv
Element-list-nonempty-p
Elementlist-projection
Element-equiv
Generic-eval-requirement
Element-list-fix
Elementlist-mapappend
Element-fix
Outelement-list-p
Outelement-p
Element-xformer
Element-listxformer
Element-p
Def-listp-rule
Def-projection-rule
Def-nonempty-listp-rule
Def-mapappend-rule
Def-listfix-rule
Rev
Defsort
List-fix
Std/lists/nth
Hons-remove-duplicates
Std/lists/update-nth
Set-equiv
Duplicity
Prefixp
Std/lists/take
Std/lists/intersection$
Nats-equiv
Repeat
Index-of
All-equalp
Sublistp
Std/lists/nthcdr
Listpos
List-equiv
Final-cdr
Std/lists/append
Std/lists/remove
Subseq-list
Rcons
Std/lists/revappend
Std/lists/remove-duplicates-equal
Std/lists/reverse
Std/lists/last
Std/lists/resize-list
Flatten
Suffixp
Std/lists/butlast
Std/lists/set-difference
Std/lists/len
Std/lists/intersectp
Std/lists/true-listp
Intersectp-witness
Subsetp-witness
Std/lists/remove1-equal
Rest-n
First-n
Std/lists/union
Append-without-guard
Std/lists/subsetp
Std/lists/member
Std/alists
Obags
Std/util
Std/strings
Std/io
Std/osets
Std/basic
Std/system
Std/typed-lists
Std/bitsets
Std/testing
Std/typed-alists
Std/stobjs
Std-extensions
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Std/lists/abstract
Def-nonempty-listp-rule
Define a theorem and save it in a table, denoting that it is a rule about element-list-nonempty-p.