Documentation

Lean.Meta.Sym.ReplaceS

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

source
@[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.

Instances For
    source
    @[inline]
    def Lean.Meta.Sym.replaceS (e : Expr) (f : Expr → Nat → Internal.AlphaShareBuilderM (Option Expr)) :
    SymM Expr
    Instances For