A version of replace_fn.h that ensures the resulting expression is maximally shared.

@[inline]

def Lean.Meta.Sym.replaceS' (e : Expr) (f : Expr → Nat → Internal.AlphaShareBuilderM (Option Expr)) : Internal.AlphaShareBuilderM Expr

Similar to replace_fn in the kernel, but assumes input is maximally shared, and ensures output is also maximally shared.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.Meta.Sym.replaceS (e : Expr) (f : Expr → Nat → Internal.AlphaShareBuilderM (Option Expr)) : SymM Expr

Equations

• Lean.Meta.Sym.replaceS e f = Lean.Meta.Sym.Internal.liftBuilderM (Lean.Meta.Sym.replaceS' e f)