Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Std/lists
Std/alists
Obags
Std/util
Defprojection
Deflist
Defaggregate
Define
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
Defenum
Add-io-pairs
Defalist
Defmapappend
Returns-specifiers
Defarbrec
Define-sk
Error-value-tuples
Defmax-nat
Defines
Defmin-int
Deftutorial
Extended-formals
Defrule
Defval
Defsurj
Defiso
Defconstrained-recognizer
Deffixer
Defmvtypes
Defconsts
Support
Defthm-signed-byte-p
Defthm-unsigned-byte-p
Defthm-natp
Defund-sk
Defmacro+
Defsum
Defthm-commutative
Definj
Defirrelevant
Defredundant
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
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.