Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
C
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Std-extensions
Std/util-extensions
Defmapping
Defsurj
Defiso
Defmapping-implementation
Defmapping-event-generation
Defmapping-check-redundancy
Defmapping-table
Defmapping-fn
Defmapping-input-processing
Defmapping-process-thm-names
Defmapping-process-inputs
Defmapping-process-function
Defmapping-process-functions
Defmapping-process-thm-enable
Defmapping-thm-keywords
Defmapping-process-name
Defmapping-macro-definition
Definj
Error-value-tuples
Defmax-nat
Defmin-int
Deftutorial
Defsurj
Defiso
Defund-sk
Defthm-commutative
Definj
Std/system-extensions
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Defmapping-implementation
Defmapping-input-processing
Input processing performed by
defmapping
.
See
input processing
for general background.
Subtopics
Defmapping-process-thm-names
Process the
:thm-names
input.
Defmapping-process-inputs
Process all the inputs.
Defmapping-process-function
Process one of the input functions (i.e.
doma
,
domb
,
alpha
, or
beta
).
Defmapping-process-functions
Process the
doma
,
domb
,
alpha
, and
beta
inputs.
Defmapping-process-thm-enable
Process the
:thm-enable
input.
Defmapping-thm-keywords
Keywords that identify all the theorems to generate.
Defmapping-process-name
Process the
name
input.