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
Warnings
Primitives
Use-set
Syntax
Getting-started
Utilities
Loader
Transforms
Expression-sizing
Occform
Oprewrite
Expand-functions
Vl-expr-expand-function-calls
Vl-expand-function-call
Vl-module-expand-functions
Vl-modulelist-expand-functions
Vl-check-bad-funcalls
Vl-funtemplate
Vl-funtemplate-p
Vl-fun-vardecllist-to-vardecls
Vl-funinputlist-to-vardecls
Vl-fundecl-expansion-template
Vl-funinput-to-vardecl
Vl-fundecllist-expansion-templates
Vl-fun-vardecllist-types-okp
Vl-portdecllist-types-okp
Vl-fun-vardecl-to-vardecl
Vl-find-funtemplate
Vl-funtemplatelist
Vl-funtemplatelist-fix
Vl-funtemplatelist-equiv
Vl-funtemplatelist-p
Vl-funtemplate-fix
Vl-funtemplate-equiv
Make-vl-funtemplate
Vl-funtemplate->locals
Vl-funtemplate->inputs
Vl-funtemplate->assigns
Change-vl-funtemplate
Vl-funtemplate->out
Vl-funtemplate->name
Vl-funbody-to-assignments
Vl-assignlist->rhses
Vl-fundecl-expand-params
Vl-fun-stmt-okp
Vl-fundecllist-expand-params
Vl-remove-fake-function-vardecls
Vl-design-expand-functions
Delayredux
Unparameterization
Caseelim
Split
Selresolve
Weirdint-elim
Vl-delta
Replicate-insts
Rangeresolve
Propagate
Clean-selects
Clean-params
Blankargs
Inline-mods
Expr-simp
Trunc
Always-top
Gatesplit
Gate-elim
Expression-optimization
Elim-supplies
Wildelim
Drop-blankports
Clean-warnings
Addinstnames
Custom-transform-hooks
Annotate
Latchcode
Elim-unused-vars
Problem-modules
Lint
Mlib
Server
Kit
Printer
Esim-vl
Well-formedness
Sv
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vl-funtemplate-p
Vl-funtemplatelist
A list of
vl-funtemplate-p
objects.
This is an ordinary
fty::deflist
.
Subtopics
Vl-funtemplatelist-fix
(vl-funtemplatelist-fix x)
is a usual
ACL2::fty
list fixing function.
Vl-funtemplatelist-equiv
Basic equivalence relation for
vl-funtemplatelist
structures.
Vl-funtemplatelist-p
(vl-funtemplatelist-p x)
recognizes lists where every element satisfies
vl-funtemplate-p
.