Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Apt
Simplify-defun
Isodata
Isodata-implementation
Isodata-event-generation
Isodata-fn
Isodata-input-processing
Isodata-symbol-isomap-alistp
Isodata-isomapp
Isodata-isomap
Make-isodata-isomap
Honsed-isodata-isomap
Change-isodata-isomap
Make-honsed-isodata-isomap
Isodata-isomap->oldp-guard
Isodata-isomap->oldp
Isodata-isomap->newp-guard
Isodata-isomap->newp
Isodata-isomap->localp
Isodata-isomap->isoname
Isodata-isomap->hints
Isodata-isomap->forth-of-back
Isodata-isomap->forth-injective
Isodata-isomap->forth-image
Isodata-isomap->forth-guard
Isodata-isomap->forth
Isodata-isomap->back-of-forth
Isodata-isomap->back-injective
Isodata-isomap->back-image
Isodata-isomap->back-guard
Isodata-isomap->back
Isodata-pos-isomap-alistp
Isodata-process-iso
Isodata-process-inputs
Isodata-process-arg/res-list-iso
Isodata-process-isomaps
Isodata-fresh-defiso-thm-names
Isodata-process-arg/res-list
Isodata-process-arg/res-list-iso-list
Isodata-process-res
Isodata-fresh-defiso-name-with-*s-suffix
Isodata-process-newp-of-new-name
Isodata-process-isomaps-ress
Isodata-process-isomaps-args
Isodata-process-arg/res-list-iso-add-ress
Isodata-process-arg/res-list-iso-add-args
Isodata-process-old
Isodata-process-undefined
Isodata-process-arg/res-list-aux
Isodata-isomap-listp
Isodata-fresh-defiso-name-with-*s-suffix-aux
Isodata-macro-definition
Tailrec
Schemalg
Restrict
Expdata
Casesplit
Simplify-term
Simplify-defun-sk
Parteval
Solve
Wrap-output
Propagate-iso
Simplify
Finite-difference
Drop-irrelevant-params
Copy-function
Lift-iso
Rename-params
Utilities
Simplify-term-programmatic
Simplify-defun-sk-programmatic
Simplify-defun-programmatic
Simplify-defun+
Common-options
Common-concepts
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
C
Java
Taspi
Bitcoin
Des
Ethereum
Sha-2
Yul
Zcash
Proof-checker-itp13
Bigmem
Regex
ACL2-programming-language
Json
X86isa
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Builtins
Axe
Execloader
Solidity
Paco
Concurrent-programs
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Isodata-isomapp
Isodata-isomap->oldp-guard
Access the
oldp-guard
field of a
isodata-isomapp
structure.