Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Recursion-and-induction
Hons-and-memoization
Events
Parallelism
History
Programming
Operational-semantics
Real
Start-here
Debugging
Miscellaneous
Term
Lambda
Pseudo-termp
Pseudo-term-fty
Pseudo-term-lambda
Pseudo-term-call
Pseudo-term-fncall
Pseudo-lambda
Pseudo-term-var
Pseudo-term-quote
Pseudo-term-kind
Pseudo-term-null
Pseudo-fnsym
Pseudo-term-case
Pseudo-term-count
Def-ev-pseudo-term-fty-support
Def-ev-pseudo-term-congruence
Pseudo-term-fix
Pseudo-var
Pseudo-term-list-fix
Pseudo-fn
Pseudo-fn-fix
Pseudo-fn-p
Std/typed-lists/pseudo-term-listp
Term-order
Pseudo-term-listp
Guard-holders
Termp
Termify
L<
Kwote
Kwote-lst
Ld
Hints
Type-set
Ordinals
Clause
ACL2-customization
With-prover-step-limit
Set-prover-step-limit
With-prover-time-limit
Local-incompatibility
Set-case-split-limitations
Subversive-recursions
Specious-simplification
Defsum
Oracle-timelimit
Thm
Defopener
Gcl
Case-split-limitations
Set-gc-strategy
Default-defun-mode
Top-level
Reader
Ttags-seen
Adviser
Ttree
Abort-soft
Defsums
Gc$
With-timeout
Coi-debug::fail
Expander
Gc-strategy
Coi-debug::assert
Sin-cos
Def::doc
Syntax
Subversive-inductions
Output-controls
Macros
Interfacing-tools
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Pseudo-term-fty
Pseudo-fn
Type of a function (either symbol or lambda), used in pseudo-term FTY support.
Subtopics
Pseudo-fn-fix
Pseudo-fn-p