		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Scopesubst

Scope aware substitution that replaces occurrences of resolved parameters with their values.

Subtopics

Vl-paramvaluelist-scopesubst: (vl-paramvaluelist-scopesubst x ss) maps vl-paramvalue-scopesubst across a list.
Vl-packeddimensionlist-scopesubst: (vl-packeddimensionlist-scopesubst x ss) maps vl-packeddimension-scopesubst across a list.
Vl-namedparamvaluelist-scopesubst: (vl-namedparamvaluelist-scopesubst x ss) maps vl-namedparamvalue-scopesubst across a list.
Vl-paramdecllist-scopesubst: (vl-paramdecllist-scopesubst x ss) maps vl-paramdecl-scopesubst across a list.
Vl-portdecllist-scopesubst: (vl-portdecllist-scopesubst x ss) maps vl-portdecl-scopesubst across a list.
Vl-plainarglist-scopesubst: (vl-plainarglist-scopesubst x ss) maps vl-plainarg-scopesubst across a list.
Vl-namedarglist-scopesubst: (vl-namedarglist-scopesubst x ss) maps vl-namedarg-scopesubst across a list.
Vl-gateinstlist-scopesubst: (vl-gateinstlist-scopesubst x ss) maps vl-gateinst-scopesubst across a list.
Vl-enumitemlist-scopesubst: (vl-enumitemlist-scopesubst x ss) maps vl-enumitem-scopesubst across a list.
Vl-vardecllist-scopesubst: (vl-vardecllist-scopesubst x ss) maps vl-vardecl-scopesubst across a list.
Vl-modinstlist-scopesubst: (vl-modinstlist-scopesubst x ss) maps vl-modinst-scopesubst across a list.
Vl-initiallist-scopesubst: (vl-initiallist-scopesubst x ss) maps vl-initial-scopesubst across a list.
Vl-fundecllist-scopesubst: (vl-fundecllist-scopesubst x ss) maps vl-fundecl-scopesubst across a list.
Vl-modulelist-scopesubst: (vl-modulelist-scopesubst x ss) maps vl-module-scopesubst across a list.
Vl-evatomlist-scopesubst: (vl-evatomlist-scopesubst x ss) maps vl-evatom-scopesubst across a list.
Vl-assignlist-scopesubst: (vl-assignlist-scopesubst x ss) maps vl-assign-scopesubst across a list.
Vl-alwayslist-scopesubst: (vl-alwayslist-scopesubst x ss) maps vl-always-scopesubst across a list.
Vl-rangelist-scopesubst: (vl-rangelist-scopesubst x ss) maps vl-range-scopesubst across a list.
Vl-aliaslist-scopesubst: (vl-aliaslist-scopesubst x ss) maps vl-alias-scopesubst across a list.
Vl-portlist-scopesubst: (vl-portlist-scopesubst x ss) maps vl-port-scopesubst across a list.
Vl-expr-scopesubst: Substitute resolved parameters into an expression.
Vl-stmt-scopesubst: Scopesubstitute into a vl-stmt-p
Vl-maybe-delayoreventcontrol-scopesubst: Scopesubstitute into a vl-maybe-delayoreventcontrol-p.
Vl-delayoreventcontrol-scopesubst: Scopesubstitute into a vl-delayoreventcontrol-p.
Vl-repeateventcontrol-scopesubst: Scopesubstitute into a vl-repeateventcontrol-p.
Vl-maybe-packeddimension-scopesubst: Scopesubstitute into a vl-maybe-packeddimension-p.
Vl-packeddimension-scopesubst: Scopesubstitute into a vl-packeddimension-p.
Vl-namedparamvalue-scopesubst: Scopesubstitute into a vl-namedparamvalue-p.
Vl-module-scopesubst: Scopesubstitute into a vl-module-p.
Vl-modelement-scopesubst: Scopesubstitute into a vl-modelement-p.
Vl-paramtype-scopesubst: Scopesubstitute into a vl-paramtype-p.
Vl-maybe-paramvalue-scopesubst: Scopesubstitute into a vl-maybe-paramvalue-p.
Vl-maybe-gatedelay-scopesubst: Scopesubstitute into a vl-maybe-gatedelay-p.
Vl-fundecl-scopesubst: Scopesubstitute into a vl-fundecl-p.
Vl-regularport-scopesubst: Scopesubstitute into a vl-regularport-p.
Vl-paramvalue-scopesubst: Scopesubstitute into a vl-paramvalue-p.
Vl-paramdecl-scopesubst: Scopesubstitute into a vl-paramdecl-p.
Vl-paramargs-scopesubst: Scopesubstitute into a vl-paramargs-p.
Vl-modinst-scopesubst: Scopesubstitute into a vl-modinst-p.
Vl-maybe-datatype-scopesubst: Scopesubstitute into a vl-maybe-datatype-p.
Vl-interfaceport-scopesubst: Scopesubstitute into a vl-interfaceport-p.
Vl-gateinst-scopesubst: Scopesubstitute into a vl-gateinst-p.
Vl-gatedelay-scopesubst: Scopesubstitute into a vl-gatedelay-p.
Vl-eventcontrol-scopesubst: Scopesubstitute into a vl-eventcontrol-p.
Vl-enumbasetype-scopesubst: Scopesubstitute into a vl-enumbasetype-p.
Vl-delaycontrol-scopesubst: Scopesubstitute into a vl-delaycontrol-p.
Vl-assign-scopesubst: Scopesubstitute into a vl-assign-p.
Vl-arguments-scopesubst: Scopesubstitute into a vl-arguments-p.
Vl-vardecl-scopesubst: Scopesubstitute into a vl-vardecl-p.
Vl-portdecl-scopesubst: Scopesubstitute into a vl-portdecl-p.
Vl-plainarg-scopesubst: Scopesubstitute into a vl-plainarg-p.
Vl-namedarg-scopesubst: Scopesubstitute into a vl-namedarg-p.
Vl-maybe-range-scopesubst: Scopesubstitute into a vl-maybe-range-p.
Vl-initial-scopesubst: Scopesubstitute into a vl-initial-p.
Vl-enumitem-scopesubst: Scopesubstitute into a vl-enumitem-p.
Vl-range-scopesubst: Scopesubstitute into a vl-range-p.
Vl-port-scopesubst: Scopesubstitute into a vl-port-p.
Vl-maybe-expr-scopesubst: Scopesubstitute into a vl-maybe-expr-p.
Vl-evatom-scopesubst: Scopesubstitute into a vl-evatom-p.
Vl-always-scopesubst: Scopesubstitute into a vl-always-p.
Vl-alias-scopesubst: Scopesubstitute into a vl-alias-p.