Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Xdoc
Undocumented
Interp-flags
Simpcode
Npn4
Cutinfo
Glcp-config-p
Glmc-config-p
Defsvtv-args
Vl-renaming-alist-p
Vcd-pathmap-p
Vcd-idxhash-p
*atc-exec-binary-strict-pure-rules*
Ecut-wirename-alistp
Context
Incremental-extremize-config-p
Block-headerp
Ctrex-rule
Execution-environmentp
Glmc-fsm-p
Transactionp
Eqbylbp-config-p
Proof-obligation
Cgraph-edge
Wcp-instance-rule-p
Fgl-casesplit-config
Wcp-witness-rule-p
Obligation-hyp
Vl-parsestate
Ecutnames-p
Te-args
Fgl-satlink-monolithic-sat-config
Fn-info-elt-p
Wcp-template-p
Truth-idx
Polarity4
Phase-fsm-params
Propiso-info-p
Cutscore
Vl-rhs
Truth6
Constraint-tuple
Truth5
Truth4
Truth3
Svexl-node
Ringosc3
Prof-entry-p
Constraint-tuple-p
Fgl-rune
Stv-spec-p
Run-snippet-file-info
Svex-scc-consts
Fsm
Machine-statep
Xor-signature-p
Run-snippet-info
Svtv-precompose-data
Pipeline-setup
Maybe-svar-p
Svl-module
Maybe-fgl-generic-rule
Frames
Maybe-snippet-mismatch
Cpuid-info-p
Vl-warningtree
Maybe-proof-obligation
Svtv-override-check
Maybe-svtv-chase-evaldata
Fty-info
Prof-entry
Substatep
Vl-maybe-rhs
Vl-parsed-ports
Svex-context
Account-statep
Maybe-simpcode
Maybe-rational
Maybe-svex
Flatten-res
Svex-reduce-config
Fty-type
Rewrite
Snippet-info
Addnames-indices
Svtv*-phase
Segment-driver
Satlink-parser-state
Fgl-binder-rune
Congruence-rule
Snippet-mismatch
Vl-ctxexpr
Rsh-of-concat-table
Chase-position
Hyp-tuple-p
Glcp-obj-ctrex-p
Glcp-bit-ctrex-p
Block$-p
Boundrw-subst-p
Svtv-cyclephase
Svar-split
Scopetree
Flatnorm-res
Fgl-rule
Constraint-rule
Vl-user-paramsetting
Svtv-override-triple
Svtv-evaldata
Svtv-composedata
Width-of-svex-extn
Array-fieldinfo-p
Wcp-example-app-p
Svtv*-input
Svex-override-triple
Svar-override-triple
3col4vecline
Constraint-rule-p
Vl-parsed-ports
Svtv-chase-evaldata
Svtv-assigns-override-config
Svex/index
Svl-env
Svl-aliasdb
Inverter
Fgl-binder-rule
Bvar-db-consistency-error
Wcp-lit-actions-p
Vcd-multivector-p
Svtv-fsm
Svexl
Constraint-instance
Vl-parsestate
Partsum-comp
Classname/params
Vcd-vector-p
Tmp-occ
Svl-occ
Svexllist
Svexl-alist
Integerp-of-svex-extn
Uninterpreted
Rw-pair
Vl-echar-raw
Vl-echar-raw
Use-set
Svtv-probe
Svex-phase-varname
Svex-cycle-varname
Range
Phase-fsm-config
Overridekey-syntaxcheck-data
Constraint
Alias
Sig
Sandwich
Cgraph-derivstate
Candidate-assign
Svex-alist-eval-equiv!
Svex-alist-eval-equiv
Scalar-fieldinfo-p
Fe-list-listp
Fgl-ev-congruence-rulelist-correct-p
N-outputs-dom-supergates-sweep-config
Svex-envlists-equivalent
Svex-alistlist-eval-equiv
Flatnorm-setup
G-map-tag
Obs-sdom-array
Dom-supergates-sweep-config
Truth4arr
Npn4arr
Syndef::acid4
Svex-envlists-similar
Svex-alist-compose-equiv
Sym-prod
Fgl-congruence-rune
Svex-envs-1mask-equiv
U32arr
Litarr
Aigtrans
Svexlist-eval-equiv
N-outputs-unreachability-config
Svex-eval-equiv
Unreachability-config
Keys-equiv
Vl-maybe-exprtype-list-p
Svex-alistlist
Svar-overridetype-p
Vcd-indexlist-p
Alternative-spec-listp
Variable-listp
Vcd-vectorlist-p
Vcd-multivectorlist-p
Field-spec-listp
Neteval-ordering
Prof-entrylist-p
Hyp-tuplelist-p
Glcp-obj-ctrexlist-p
Symbol-path-list-p
Pseudo-input-listp
Input-listp
Ecutname-list-p
Boundrw-substlist-p
Constraintlist
Fgl-object-bindings
Fgl-generic-rule
4v-equiv
Sdm-instruction-table
Svexl-node-array
Sig-path
Func-alist
Fgl-generic-rune
Fgl-ev-iff-equiv
Pseudo-term-subst
Nth-lit-equiv
Frames-equiv
Eval-formula-equiv
Svex-s4env
Svex-env-keys-equiv
Svex-alist-keys-equiv
Pseudo-term-alist
Fgl-ev-equiv
Lits-equiv
Nth-nat-equiv
Faig-const-equiv
Bdd-equiv
Byte-list
Vl-user-paramsettings
Classname/params-unparam-map
Obligation-hyp-list
Svtv*-output-alist
Svtv*-input-alist
Svtv-probealist
Svtv-override-triplemap
Svtv-cyclephaselist
Svex/index-maybenat-alist
Svex-context-alist
Segment-driver-map
Rangemap
Fnsym-svexlistlist-alist
Tmp-occ-alist
Svl-module-alist
Svexl-node-alist
Occ-name-alist
Integerp-of-svex-extn-list
Alias-alist
Special-char-alist
Fty-info-alist
Bfr-updates
Term-equivs
Term-bvars
Sig-table
Fn-indices
Fgl-function-mode-alist
Ctrex-ruletable
Constraint-db
Congruence-rule-table
Cgraph-derivstates
Cgraph-alist
Cgraph
Casesplit-alist
Truthmap
Named-lit-list-map
Axi-map
Nth-equiv
Faig-fix-equiv
Vl-string/int-alist
Vl-reservedtable
Vl-echarlist
Vl-ctxexprlist
Vl-coredatatype-infolist
Vl-usertypes
Vl-coredatatype-infolist
Proof-obligation-list
Use-set-summaries
Svtv-rev-probealist
Svex/index-nat-alist
Svex/index-key-alist
Svex-key-alist
Svex-envlist
Svar-widths
Svar-widths-fix
Svar-widths-p
Svar-widths-equiv
Svar-width-map
Svar-splittab
Svar-proplist
Svar-key-alist
Rsh-of-concat-alist
Path-alist
Name-alist
Address-alist
Width-of-svex-extn-list
Svl-occ-alist
Svex-to-natp-alist
Symbol-string-alist
Symbol-integer-alist
Sym-nat-alist
String-string-alist
Fty-types
Fty-field-alist
Any-table
Obj-alist
Nat-nat-alist
Constraint-instancelist
Congruence-rulelist
Calist
Bvar-db-consistency-errorlist
Var-counts-alist
Pseudo-var-list
Equiv-contextslist
Nat-val-alistp
Id-neg-alist
String-keyed-alist-p
Snippet-table
Snippet-mismatch-list
Vl-reportcardkeylist
Partsumlist
Partsum-elt
Classname/paramslist
Vl-reportcardkeylist
Vl-locationlist
Vl-echarlist
Perm4-list
Svtv*-phaselist
Svtv-override-triplemaplist
Svtv-override-triplelist
Svtv-override-checklist
Svtv-name-lhs-map-list
Svex/indexlist
Svexlistlist
Svex-override-triplelist
Svex-contextlist
Svarlist-list
Svar-widthslist
Svar-overridetypelist
Svar-override-triplelist
Segment-driverlist
Rangelist
Chase-stack
Addresslist
4veclistlist
3col4vecs
Occ-name-list
Alias-lst
Word-list
Sig-path-list
Function-option-name-lst
Any-trace
Bfr-varnamelist
Aig-varlist
Scratch-nontagidxlist
Prof-entrylist
Interp-st-field-p
Fgl-runelist
Fgl-rulelist
Fgl-object-bindingslist
Fgl-congruence-runelist
Fgl-binder-runelist
Fgl-binder-rulelist
Ctrex-rulelist
Constraint-tuplelist
Cgraph-edgelist
Candidate-assigns
Rw-pairlist
Rewritelist
Equiv-contexts
Bindinglist
Pos-list
Obs-sdom-info-list
Cutinfolist
Bit-list
Axi-termlist
Axi-litlist
Symbol-pseudoterm-alist
Symbol-pseudoeventform-alist
Inst-list
Vl-user-paramsettings-mode-p
Svtv-data$c-field-p
Ctrex-ruletype-p
String-stringlist-alist
Ipasir-status-p
Fgl-toplevel-sat-check-mode-p
Axi-op-p
Vl-opacity-p
St-hyp-method-p
Scratchobj-kind-p
Logicman-field-p
Bvar-db$c-field-p
Env$-field-p
Axi
*smt-architecture*
*vl-directions-kwds*
*vl-directions-kwd-alist*
Rlp-trees
Save
Defsection
Markup
Preprocessor
Terminal
Emacs-links
Defxdoc
Katex-integration
Constructors
Entities
Defxdoc+
Save-rendered
Add-resource-directory
Testing
Order-subtopics
Save-rendered-event
Archive-matching-topics
Archive-xdoc
Xdoc-extend
Set-default-parents
Missing-parents
Defpointer
Defxdoc-raw
Xdoc-tests
Xdoc-prepend
Defsection-progn
Gen-xdoc-for-file
ACL2-doc
Recursion-and-induction
Loop$-primer
Operational-semantics
Pointers
Doc
Documentation-copyright
Course-materials
Args
ACL2-doc-summary
Finding-documentation
Broken-link
Doc-terminal-test-2
Doc-terminal-test-1
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Undocumented
Svar-widths
An alist mapping
svar-p
to
integerp
.
This is an ordinary
defalist
.
Subtopics
Svar-widths-fix
(svar-widths-fix x)
is an
fty
alist fixing function that follows the fix-keys strategy.
Svar-widths-p
Recognizer for
svar-widths
.
Svar-widths-equiv
Basic equivalence relation for
svar-widths
structures.
