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