# Helper functions for working with typed syntaxes. #

source
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

Instances For