Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Sv
Svex-stvs
Svex-decomposition-methodology
Sv-versus-esim
Svex-decomp
Svex-compose-dfs
Svex-compilation
Moddb
Svmods
Address
Wire
Module
Lhs
Path
Svar-add-namespace
Design
Modinst
Modinst-fix
Modinst-equiv
Make-modinst
Modinst->modname
Modinst->instname
Change-modinst
Modinstlist
Modinstlist-fix
Modinstlist->instnames
Modinstlist->modnames
Modinstlist-p
Modinstlist-equiv
Modinst-p
Lhs-add-namespace
Modalist
Path-add-namespace
Modname->submodnames
Name
Constraintlist-addr-p
Svex-alist-addr-p
Svar-map-addr-p
Lhspairs-addr-p
Modname
Assigns-addr-p
Lhs-addr-p
Lhatom-addr-p
Modhier-list-measure
Attributes
Modhier-measure
Modhier-list-measure-aux
Modhier-loopfreelist-p
Modhier-loopfree-p
Svstmt
Sv-tutorial
Expressions
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Modinst
Modinstlist
A list of
modinst-p
objects.
This is an ordinary
deflist
.
Subtopics
Modinstlist-fix
(modinstlist-fix x)
is a usual
fty
list fixing function.
Modinstlist->instnames
(modinstlist->instnames x)
maps
modinst->instname
across a list.
Modinstlist->modnames
(modinstlist->modnames x)
maps
modinst->modname
across a list.
Modinstlist-p
(modinstlist-p x)
recognizes lists where every element satisfies
modinst-p
.
Modinstlist-equiv
Basic equivalence relation for
modinstlist
structures.