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.
• Lean.Meta.Sym.replaceS' (Lean.Expr.lit a) f = do let __do_lift ← f (Lean.Expr.lit a) 0 match __do_lift with | some r => pure r | x => pure (Lean.Expr.lit a)
• Lean.Meta.Sym.replaceS' (Lean.Expr.mvar mvarId) f = do let __do_lift ← f (Lean.Expr.mvar mvarId) 0 match __do_lift with | some r => pure r | x => pure (Lean.Expr.mvar mvarId)
• Lean.Meta.Sym.replaceS' (Lean.Expr.fvar fvarId) f = do let __do_lift ← f (Lean.Expr.fvar fvarId) 0 match __do_lift with | some r => pure r | x => pure (Lean.Expr.fvar fvarId)
• Lean.Meta.Sym.replaceS' (Lean.Expr.sort u) f = do let __do_lift ← f (Lean.Expr.sort u) 0 match __do_lift with | some r => pure r | x => pure (Lean.Expr.sort u)
• Lean.Meta.Sym.replaceS' e f = do let __do_lift ← f e 0 match __do_lift with | some r => pure r | x => StateT.run' (Lean.Meta.Sym.visit✝ e 0 f) ∅

@[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)