Documentation

StrataDDM.TaggedRegions

source
def StrataDDM.ExternParser.mkParser (n : Lean.SyntaxNodeKind) (startToken endToken : String) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def StrataDDM.ExternParser.mkParser.formatter (sym : Lean.Name) :
    Lean.PrettyPrinter.FormatterM Unit
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def StrataDDM.ExternParser.mkParser.parenthesizer :
      Lean.Name → (sym : String) → Lean.PrettyPrinter.ParenthesizerM Unit
      Equations
      Instances For
        source
        def StrataDDM.ExternParser.declareTaggedRegion :
        Lean.ParserDescr

        This creates declares a parser that recognizes text within a set of tags.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def StrataDDM.ExternParser.declareTaggedRegionImpl :
          Lean.Elab.Command.CommandElab
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For