Helper functions for working with typed syntaxes. #
def
Lean.TSyntax.replaceM
{M : Type → Type}
{k : Lean.SyntaxNodeKinds}
[inst : 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.
Equations
- Lean.TSyntax.replaceM f stx = Lean.TSyntax.mk <$> Lean.Syntax.replaceM f stx.raw
def
Lean.Syntax.TSepArray.ofElems
{k : Lean.SyntaxNodeKinds}
{sep : String}
(elems : Array (Lean.TSyntax k))
:
Lean.Syntax.TSepArray k sep
Constructs a typed separated array from elements. The given array does not include the separators.
Like Syntax.SepArray.ofElems but for typed syntax.
Equations
- Lean.Syntax.TSepArray.ofElems elems = { elemsAndSeps := (Lean.Syntax.SepArray.ofElems (Lean.TSyntaxArray.raw elems)).elemsAndSeps }