Helper functions for working with typed syntaxes.

def Lean.TSyntax.replaceM {M : Type → Type} {k : SyntaxNodeKinds} [Monad M] (f : Syntax → M (Option Syntax)) (stx : TSyntax k) : M (TSyntax k)

Applies the given function to every subsyntax.

Like Syntax.replaceM but for typed syntax. (Note there are no guarantees of type correctness here.)

Equations

• Lean.TSyntax.replaceM f stx = Lean.TSyntax.mk <$> Lean.Syntax.replaceM f stx.raw