Documentation

Mathlib.Util.Syntax

Helper functions for working with typed syntaxes. #

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

Applies the given function to every subsyntax.

Like Syntax.replaceM but for typed syntax.

Equations

Constructs a typed separated array from elements. The given array does not include the separators.

Like Syntax.SepArray.ofElems but for typed syntax.

Equations