Struct WKVarSubst 

pub struct WKVarSubst {
    pub subst_instantiations: UnordMap<WKVid, Vec<Expr>>,
    pub wkvar_instantiations: UnordMap<WKVid, Binder<Expr>>,
    pub keep_wkvars: bool,
}

Fields

subst_instantiations: UnordMap<WKVid, Vec<Expr>>

A map from wkvid to each of the substitutions we made for it in whatever we folded over.

In theory there should only ever be one value in this map.

wkvar_instantiations: UnordMap<WKVid, Binder<Expr>>

keep_wkvars: bool

Keep wkvars after substituting

Implementations

impl WKVarSubst

pub fn new( wkvar_instantiations: UnordMap<WKVid, Binder<Expr>>, keep_wkvars: bool, ) -> Self

Trait Implementations

impl TypeFolder for WKVarSubst

fn fold_expr(&mut self, e: &Expr) -> Expr

fn enter_binder(&mut self, _vars: &Interned<[BoundVariableKind]>)

fn exit_binder(&mut self)

fn fold_sort(&mut self, sort: &Sort) -> Sort

fn fold_ty(&mut self, ty: &Ty) -> Ty

fn fold_bty(&mut self, bty: &BaseTy) -> BaseTy

fn fold_subset_ty(&mut self, constr: &SubsetTy) -> SubsetTy

fn fold_region(&mut self, re: &Region) -> Region

fn fold_const(&mut self, c: &Const) -> Const