Helper functions for working with typed syntaxes. #
def
Lean.TSyntax.replaceM
{M : Type → Type}
{k : Lean.SyntaxNodeKinds}
[Monad M]
(f : Lean.Syntax → M (Option Lean.Syntax))
(stx : Lean.TSyntax k)
:
M (Lean.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