def Lean.Doc.Parser.skipFn : Parser.ParserFn

A parser that does nothing.

Equations

• Lean.Doc.Parser.skipFn x✝ s = s

def Lean.Doc.Parser.ignoreFn (p : Parser.ParserFn) : Parser.ParserFn

Parses as p, but discards the result.

Equations

• Lean.Doc.Parser.ignoreFn p c s = (p c s).shrinkStack s.stxStack.size

def Lean.Doc.Parser.asStringFn (p : Parser.ParserFn) (quoted : Bool := false) (transform : String → String := id) : Parser.ParserFn

Match an arbitrary Parser and return the consumed String in a Syntax.atom.

Equations

• Lean.Doc.Parser.asStringFn p quoted transform c s = if (p c s).hasError = true then p c s else Lean.Doc.Parser.asStringAux✝ quoted s.pos transform c ((p c s).shrinkStack s.stxStack.size)

def Lean.Doc.Parser.fakeAtom (str : String) (info : SourceInfo := SourceInfo.none) : Parser.ParserFn

Construct a “fake” atom with the given string content and source information.

Normally, atoms are always substrings of the original input; however, Verso's concrete syntax is different enough from Lean's that this isn't always a good match.

Equations

• Lean.Doc.Parser.fakeAtom str info _c s = s.pushSyntax (Lean.Syntax.atom info str)

inductive Lean.Doc.Parser.OrderedListType : Type

Ordered lists may have two styles of indicator, with trailing dots or parentheses.

• numDot : OrderedListType

  Items like 1.

• parenAfter : OrderedListType

  Items like 1)

instance Lean.Doc.Parser.instReprOrderedListType : Repr OrderedListType

Equations

• Lean.Doc.Parser.instReprOrderedListType = { reprPrec := Lean.Doc.Parser.instReprOrderedListType.repr }

def Lean.Doc.Parser.instReprOrderedListType.repr : OrderedListType → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.instBEqOrderedListType.beq : OrderedListType → OrderedListType → Bool

Equations

• Lean.Doc.Parser.instBEqOrderedListType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lean.Doc.Parser.instBEqOrderedListType : BEq OrderedListType

Equations

• Lean.Doc.Parser.instBEqOrderedListType = { beq := Lean.Doc.Parser.instBEqOrderedListType.beq }

instance Lean.Doc.Parser.instDecidableEqOrderedListType : DecidableEq OrderedListType

Equations

• Lean.Doc.Parser.instDecidableEqOrderedListType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Lean.Doc.Parser.instOrdOrderedListType : Ord OrderedListType

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.Doc.Parser.UnorderedListType : Type

Unordered lists may have three indicators: asterisks, dashes, or pluses.

• asterisk : UnorderedListType

  Items like *

• dash : UnorderedListType

  Items like -

• plus : UnorderedListType

  Items like +

instance Lean.Doc.Parser.instReprUnorderedListType : Repr UnorderedListType

Equations

• Lean.Doc.Parser.instReprUnorderedListType = { reprPrec := Lean.Doc.Parser.instReprUnorderedListType.repr }

def Lean.Doc.Parser.instReprUnorderedListType.repr : UnorderedListType → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Doc.Parser.instBEqUnorderedListType : BEq UnorderedListType

Equations

• Lean.Doc.Parser.instBEqUnorderedListType = { beq := Lean.Doc.Parser.instBEqUnorderedListType.beq }

def Lean.Doc.Parser.instBEqUnorderedListType.beq : UnorderedListType → UnorderedListType → Bool

Equations

• Lean.Doc.Parser.instBEqUnorderedListType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lean.Doc.Parser.instDecidableEqUnorderedListType : DecidableEq UnorderedListType

Equations

• Lean.Doc.Parser.instDecidableEqUnorderedListType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Lean.Doc.Parser.instOrdUnorderedListType : Ord UnorderedListType

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.inlineTextChar : Parser.ParserFn

Parses a character that's allowed as part of inline text. This resolves escaped characters and performs limited lookahead for characters that only begin a different inline as part of a sequence.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.blockOpener : Parser.ParserFn

Parses block opener prefixes. At the beginning of the line, if this parser succeeds, then a special block is beginning.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.val : Parser.ParserFn

Parses an argument value, which may be a string literal, identifier, or numeric literal.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.recoverBlock (p : Parser.ParserFn) (final : Parser.ParserFn := skipFn) : Parser.ParserFn

Recovers from a parse error by skipping input until one or more complete blank lines has been skipped.

Equations

• Lean.Doc.Parser.recoverBlock p final = Lean.Parser.recoverFn p fun (x : Lean.Parser.RecoveryContext) => Lean.Doc.Parser.ignoreFn Lean.Doc.Parser.skipBlock✝ >> final

def Lean.Doc.Parser.arg : Parser.ParserFn

Parses an argument to a role, directive, command, or code block, which may be named or positional or a flag.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.args (multiline : Option Nat := none) : Parser.ParserFn

Parses zero or more arguments to a role, directive, command, or code block.

Equations

• Lean.Doc.Parser.args multiline = Lean.Parser.sepByFn true Lean.Doc.Parser.arg (Lean.Doc.Parser.nameArgWhitespace✝ multiline)

def Lean.Doc.Parser.nameAndArgs (multiline : Option Nat := none) : Parser.ParserFn

Parses a name and zero or more arguments to a role, directive, command, or code block.

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Doc.Parser.InlineCtxt : Type

The context within which a newline element is parsed.

• allowNewlines : Bool

  Are newlines allowed here?

• minIndent : Nat

  The minimum indentation of a continuation line for the current paragraph

• boldDepth : Option Nat

  How many asterisks introduced the current level of boldness? none means no bold here.

• emphDepth : Option Nat

  How many underscores introduced the current level of emphasis? none means no emphasis here.

• inLink : Bool

  Are we in a link?

def Lean.Doc.Parser.instInhabitedInlineCtxt.default : InlineCtxt

Equations

• Lean.Doc.Parser.instInhabitedInlineCtxt.default = { allowNewlines := default, minIndent := default, boldDepth := default, emphDepth := default, inLink := default }

instance Lean.Doc.Parser.instInhabitedInlineCtxt : Inhabited InlineCtxt

Equations

• Lean.Doc.Parser.instInhabitedInlineCtxt = { default := Lean.Doc.Parser.instInhabitedInlineCtxt.default }

partial def Lean.Doc.Parser.emph (ctxt : InlineCtxt) : Parser.ParserFn

Parses emphasis: a matched pair of one or more _.

partial def Lean.Doc.Parser.bold (ctxt : InlineCtxt) : Parser.ParserFn

Parses bold: a matched pair of one or more *.

def Lean.Doc.Parser.code : Parser.ParserFn

Parses inline code.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.math : Parser.ParserFn

Parses mathematics.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.text : Parser.ParserFn

Reads a prefix of a line of text, stopping at a text-mode special character.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Doc.Parser.link (ctxt : InlineCtxt) : Parser.ParserFn

Parses a link.

def Lean.Doc.Parser.footnote (ctxt : InlineCtxt) : Parser.ParserFn

Parses a footnote.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.image : Parser.ParserFn

Parses an image.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Doc.Parser.role (ctxt : InlineCtxt) : Parser.ParserFn

Parses a role.

partial def Lean.Doc.Parser.delimitedInline (ctxt : InlineCtxt) : Parser.ParserFn

Parses an inline that is self-delimiting (that is, with well-defined start and stop characters).

partial def Lean.Doc.Parser.inline (ctxt : InlineCtxt) : Parser.ParserFn

Parses any inline element.

def Lean.Doc.Parser.metadataContents : Parser.Parser

A non-meta copy of Lean.Doc.Syntax.metadataContents.

Equations

• Lean.Doc.Parser.metadataContents = Lean.Parser.Term.structInstFields (Lean.Parser.sepByIndent Lean.Parser.Term.structInstField ", " (Lean.Parser.symbol ", ") true)

def Lean.Doc.Parser.metadataBlock : Parser.ParserFn

Parses a metadata block, which contains the contents of a Lean structure initialization but is surrounded by %%% on each side.

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Doc.Parser.InList : Type

Records that the parser is presently parsing a list.

• indentation : Nat

  The indentation of list indicators.

• type : OrderedListType ⊕ UnorderedListType

  The specific list type and its indicator style

instance Lean.Doc.Parser.instReprInList : Repr InList

Equations

• Lean.Doc.Parser.instReprInList = { reprPrec := Lean.Doc.Parser.instReprInList.repr }

def Lean.Doc.Parser.instReprInList.repr : InList → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Doc.Parser.BlockCtxt : Type

The context within which a block should be valid.

• minIndent : Nat

  The block's minimum indentation.

• maxDirective : Option Nat

  The block's maximal directive size (that is, the greatest number of allowed colons).

• inLists : List InList

  The nested list context, innermost first.

def Lean.Doc.Parser.instInhabitedBlockCtxt.default : BlockCtxt

Equations

• Lean.Doc.Parser.instInhabitedBlockCtxt.default = { minIndent := default, maxDirective := default, inLists := default }

instance Lean.Doc.Parser.instInhabitedBlockCtxt : Inhabited BlockCtxt

Equations

• Lean.Doc.Parser.instInhabitedBlockCtxt = { default := Lean.Doc.Parser.instInhabitedBlockCtxt.default }

instance Lean.Doc.Parser.instReprBlockCtxt : Repr BlockCtxt

Equations

• Lean.Doc.Parser.instReprBlockCtxt = { reprPrec := Lean.Doc.Parser.instReprBlockCtxt.repr }

def Lean.Doc.Parser.instReprBlockCtxt.repr : BlockCtxt → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.lookaheadOrderedListIndicator (ctxt : BlockCtxt) (p : OrderedListType → Int → Parser.ParserFn) : Parser.ParserFn

Succeeds when the parser is looking at an ordered list indicator.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.lookaheadUnorderedListIndicator (ctxt : BlockCtxt) (p : UnorderedListType → Parser.ParserFn) : Parser.ParserFn

Succeeds when the parser is looking at an unordered list indicator.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Doc.Parser.listItem (ctxt : BlockCtxt) : Parser.ParserFn

Parses a list item according to the current nesting context.

partial def Lean.Doc.Parser.descItem (ctxt : BlockCtxt) : Parser.ParserFn

Parses an item from a description list.

partial def Lean.Doc.Parser.blockquote (ctxt : BlockCtxt) : Parser.ParserFn

Parses a block quote.

partial def Lean.Doc.Parser.unorderedList (ctxt : BlockCtxt) : Parser.ParserFn

Parses an unordered list.

partial def Lean.Doc.Parser.orderedList (ctxt : BlockCtxt) : Parser.ParserFn

Parses an ordered list.

partial def Lean.Doc.Parser.definitionList (ctxt : BlockCtxt) : Parser.ParserFn

Parses a definition list.

def Lean.Doc.Parser.para (ctxt : BlockCtxt) : Parser.ParserFn

Parses a paragraph (that is, a sequence of otherwise-undecorated inlines).

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.header (ctxt : BlockCtxt) : Parser.ParserFn

Parses a header.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.codeBlock (ctxt : BlockCtxt) : Parser.ParserFn

Parses a code block. The resulting string literal has already had the fences' leading indentation stripped.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Doc.Parser.directive (ctxt : BlockCtxt) : Parser.ParserFn

Parses a directive.

def Lean.Doc.Parser.block_command (ctxt : BlockCtxt) : Parser.ParserFn

Parses a block command.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.linkRef (c : BlockCtxt) : Parser.ParserFn

Parses a link reference target.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.footnoteRef (c : BlockCtxt) : Parser.ParserFn

Parses a footnote reference target.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Doc.Parser.block (c : BlockCtxt) : Parser.ParserFn

Parses a block.

partial def Lean.Doc.Parser.blocks (c : BlockCtxt) : Parser.ParserFn

Parses zero or more blocks.

partial def Lean.Doc.Parser.blocks1 (c : BlockCtxt) : Parser.ParserFn

Parses one or more blocks.

def Lean.Doc.Parser.document (blockContext : BlockCtxt := { }) : Parser.ParserFn

Parses some number of blank lines followed by zero or more blocks.

Equations

• Lean.Doc.Parser.document blockContext = Lean.Doc.Parser.ignoreFn (Lean.Parser.manyFn Lean.Doc.Parser.blankLine✝) >> Lean.Doc.Parser.blocks blockContext

def Lean.Doc.Parser.ifVersoFn (ifVerso ifNotVerso : Parser.ParserFn) : Parser.ParserFn

Parses as ifVerso if the option doc.verso is true, or as ifNotVerso otherwise.

Equations

• Lean.Doc.Parser.ifVersoFn ifVerso ifNotVerso c s = if Lean.KVMap.getBool c.options `doc.verso = true then ifVerso c s else ifNotVerso c s

def Lean.Doc.Parser.ifVerso (ifVerso ifNotVerso : Parser.Parser) : Parser.Parser

Parses as ifVerso if the option doc.verso is true, or as ifNotVerso otherwise.

Equations

• Lean.Doc.Parser.ifVerso ifVerso ifNotVerso = { fn := Lean.Doc.Parser.ifVersoFn ifVerso.fn ifNotVerso.fn }

def Lean.Doc.Parser.ifVerso.formatter (f1 f2 : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

Formatter for ifVerso—formats according to the underlying formatters.

Equations

• Lean.Doc.Parser.ifVerso.formatter f1 f2 = (f1 <|> f2)

def Lean.Doc.Parser.ifVerso.parenthesizer (p1 p2 : PrettyPrinter.Parenthesizer) : PrettyPrinter.Parenthesizer

Parenthesizer for ifVerso—parenthesizes according to the underlying parenthesizers.

Equations

• Lean.Doc.Parser.ifVerso.parenthesizer p1 p2 = (p1 <|> p2)

def Lean.Doc.Parser.withoutVersoSyntax (p : Parser.Parser) : Parser.Parser

Disables the option doc.verso while running a parser.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Doc.Parser.withoutVersoSyntax.formatter (p : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

Formatter for withoutVersoSyntax—formats according to the underlying formatter.

Equations

• Lean.Doc.Parser.withoutVersoSyntax.formatter p = p

def Lean.Doc.Parser.withoutVersoSyntax.parenthesizer (p : PrettyPrinter.Parenthesizer) : PrettyPrinter.Parenthesizer

Parenthesizer for withoutVersoSyntax—parenthesizes according to the underlying parenthesizer.

Equations

• Lean.Doc.Parser.withoutVersoSyntax.parenthesizer p = p