Skip to main content

substitute_ident_in_resolved_expr

Function substitute_ident_in_resolved_expr 

Source
pub fn substitute_ident_in_resolved_expr(
    expr: &Spanned<ResolvedExpr>,
    from: &str,
    to: &str,
) -> Spanned<ResolvedExpr>
Expand description

ResolvedExpr mirror of substitute_ident_in_expr. Rewrites every Ident(from) / Resolved { name: from, .. } leaf to Ident(to) — the slot identity (if any) is dropped because the substitution targets a free variable name that doesn’t have a slot in the resolver’s local table. Used by proof-mode when-redundancy check + smart-guard predicate substitution after the IR carries pre-resolved expressions.