Documentation

Lean.PrettyPrinter.Formatter

The formatter turns a Syntax tree into a Format object, inserting both mandatory whitespace (to separate adjacent tokens) as well as "pretty" optional whitespace.

The basic approach works much like the parenthesizer: A right-to-left traversal over the syntax tree, driven by parser-specific handlers registered via attributes. The traversal is right-to-left so that when emitting a token, we already know the text following it and can decide whether or not whitespace between the two is necessary.

structure Lean.PrettyPrinter.Formatter.Context:

Type

options : Lean.Options
table : Lean.Parser.TokenTable

structure Lean.PrettyPrinter.Formatter.State:

Type

stxTrav : Lean.Syntax.Traverser
leadWord : String
isUngrouped : Bool
mustBeGrouped : Bool
stack : Array Lean.Format

@[inline]

abbrev Lean.PrettyPrinter.FormatterM (α : Type) :

Type

Equations

Lean.PrettyPrinter.FormatterM = ReaderT Lean.PrettyPrinter.Formatter.Context (StateRefT' IO.RealWorld Lean.PrettyPrinter.Formatter.State Lean.CoreM)

@[inline]

def Lean.PrettyPrinter.FormatterM.orElse {α : Type} (p₁ : Lean.PrettyPrinter.FormatterM α) (p₂ : Unit → Lean.PrettyPrinter.FormatterM α) :

Lean.PrettyPrinter.FormatterM α

Equations

Lean.PrettyPrinter.FormatterM.orElse p₁ p₂ = do let s ← get Lean.catchInternalId Lean.PrettyPrinter.backtrackExceptionId p₁ fun x => do set s p₂ ()

instance Lean.PrettyPrinter.instOrElseFormatterM {α : Type} :

OrElse (Lean.PrettyPrinter.FormatterM α)

Equations

Lean.PrettyPrinter.instOrElseFormatterM = { orElse := Lean.PrettyPrinter.FormatterM.orElse }

@[inline]

abbrev Lean.PrettyPrinter.Formatter:

Type

Equations

Lean.PrettyPrinter.Formatter = Lean.PrettyPrinter.FormatterM Unit

unsafe def Lean.PrettyPrinter.mkFormatterAttribute:

IO (Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Formatter)

Equations

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

opaque Lean.PrettyPrinter.formatterAttribute:

Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Formatter

unsafe def Lean.PrettyPrinter.mkCombinatorFormatterAttribute:

IO Lean.ParserCompiler.CombinatorAttribute

Equations

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

opaque Lean.PrettyPrinter.combinatorFormatterAttribute:

Lean.ParserCompiler.CombinatorAttribute

def Lean.PrettyPrinter.Formatter.throwBacktrack {α : Type} :

Lean.PrettyPrinter.FormatterM α

Equations

Lean.PrettyPrinter.Formatter.throwBacktrack = throw (Lean.Exception.internal Lean.PrettyPrinter.backtrackExceptionId)

instance Lean.PrettyPrinter.Formatter.instMonadTraverserFormatterM:

Lean.Syntax.MonadTraverser Lean.PrettyPrinter.FormatterM

Equations

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

def Lean.PrettyPrinter.Formatter.getStack:

Lean.PrettyPrinter.FormatterM (Array Lean.Format)

Equations

Lean.PrettyPrinter.Formatter.getStack = do let st ← get pure st.stack

def Lean.PrettyPrinter.Formatter.getStackSize:

Lean.PrettyPrinter.FormatterM Nat

Equations

Lean.PrettyPrinter.Formatter.getStackSize = do let stack ← Lean.PrettyPrinter.Formatter.getStack pure (Array.size stack)

def Lean.PrettyPrinter.Formatter.setStack (stack : Array Lean.Format) :

Lean.PrettyPrinter.FormatterM Unit

Equations

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

def Lean.PrettyPrinter.Formatter.pushWhitespace (f : Lean.Format) :

Lean.PrettyPrinter.FormatterM Unit

Equations

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

def Lean.PrettyPrinter.Formatter.pushLine:

Lean.PrettyPrinter.FormatterM Unit

Equations

Lean.PrettyPrinter.Formatter.pushLine = Lean.PrettyPrinter.Formatter.pushWhitespace Lean.Format.line

def Lean.PrettyPrinter.Formatter.visitArgs (x : Lean.PrettyPrinter.FormatterM Unit) :

Lean.PrettyPrinter.FormatterM Unit

Execute x at the right-most child of the current node, if any, then advance to the left.

Equations

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

def Lean.PrettyPrinter.Formatter.fold (fn : Array Lean.Format → Lean.Format) (x : Lean.PrettyPrinter.FormatterM Unit) :

Lean.PrettyPrinter.FormatterM Unit

Execute x, pass array of generated Format objects to fn, and push result.

Equations

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

def Lean.PrettyPrinter.Formatter.concat (x : Lean.PrettyPrinter.FormatterM Unit) :

Lean.PrettyPrinter.FormatterM Unit

Execute x and concatenate generated Format objects.

Equations

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

def Lean.PrettyPrinter.Formatter.indent (x : Lean.PrettyPrinter.Formatter) (indent : optParam (Option Int) none) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.fill (x : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.group (x : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.withMaybeTag (pos? : Option String.Pos) (x : Lean.PrettyPrinter.FormatterM Unit) :

Lean.PrettyPrinter.Formatter

If pos? has a position, run x and tag its results with that position, if they are not already tagged. Otherwise just run x.

Equations

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

def Lean.PrettyPrinter.Formatter.orelse.formatter (p1 : Lean.PrettyPrinter.Formatter) (p2 : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.orelse.formatter p1 p2 = HOrElse.hOrElse p1 fun x => p2

@[extern lean_mk_antiquot_formatter]

opaque Lean.PrettyPrinter.Formatter.mkAntiquot.formatter' (name : String) (kind : Lean.SyntaxNodeKind) (anonymous : optParam Bool true) (isPseudoKind : optParam Bool false) :

Lean.PrettyPrinter.Formatter

@[extern lean_pretty_printer_formatter_interpret_parser_descr]

opaque Lean.PrettyPrinter.Formatter.interpretParserDescr':

Lean.ParserDescr → Lean.CoreM Lean.PrettyPrinter.Formatter

unsafe def Lean.PrettyPrinter.Formatter.formatterForKindUnsafe (k : Lean.SyntaxNodeKind) :

Lean.PrettyPrinter.Formatter

Equations

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

@[implementedBy Lean.PrettyPrinter.Formatter.formatterForKindUnsafe]

opaque Lean.PrettyPrinter.Formatter.formatterForKind (k : Lean.SyntaxNodeKind) :

Lean.PrettyPrinter.Formatter

def Lean.PrettyPrinter.Formatter.withAntiquot.formatter (antiP : Lean.PrettyPrinter.Formatter) (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.withAntiquot.formatter antiP p = Lean.PrettyPrinter.Formatter.orelse.formatter antiP p

def Lean.PrettyPrinter.Formatter.withAntiquotSuffixSplice.formatter:

Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.tokenWithAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.categoryFormatterCore (cat : Lean.Name) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.categoryParser.formatter (cat : Lean.Name) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.categoryFormatter (cat : Lean.Name) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.categoryFormatter cat = Lean.PrettyPrinter.Formatter.fill (Lean.PrettyPrinter.Formatter.indent (Lean.PrettyPrinter.Formatter.categoryFormatterCore cat) none)

def Lean.PrettyPrinter.Formatter.categoryParserOfStack.formatter (offset : Nat) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.parserOfStack.formatter (offset : Nat) (_prec : optParam Nat 0) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.error.formatter (_msg : String) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.error.formatter _msg = pure ()

def Lean.PrettyPrinter.Formatter.errorAtSavedPos.formatter (_msg : String) (_delta : Bool) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.errorAtSavedPos.formatter _msg _delta = pure ()

def Lean.PrettyPrinter.Formatter.atomic.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.atomic.formatter p = p

def Lean.PrettyPrinter.Formatter.lookahead.formatter:

Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.lookahead.formatter x = pure ()

def Lean.PrettyPrinter.Formatter.notFollowedBy.formatter:

Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.notFollowedBy.formatter x = pure ()

def Lean.PrettyPrinter.Formatter.andthen.formatter (p1 : Lean.PrettyPrinter.Formatter) (p2 : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.andthen.formatter p1 p2 = SeqRight.seqRight p2 fun x => p1

def Lean.PrettyPrinter.Formatter.checkKind (k : Lean.SyntaxNodeKind) :

Lean.PrettyPrinter.FormatterM Unit

Equations

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

def Lean.PrettyPrinter.Formatter.node.formatter (k : Lean.SyntaxNodeKind) (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.node.formatter k p = do Lean.PrettyPrinter.Formatter.checkKind k Lean.PrettyPrinter.Formatter.visitArgs p

def Lean.PrettyPrinter.Formatter.trailingNode.formatter (k : Lean.SyntaxNodeKind) :

Nat → Nat → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.parseToken (s : String) :

Lean.PrettyPrinter.FormatterM Lean.Parser.ParserState

Equations

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

def Lean.PrettyPrinter.Formatter.pushToken (info : Lean.SourceInfo) (tk : String) :

Lean.PrettyPrinter.FormatterM Unit

Equations

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

def Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter (sym : String) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.nonReservedSymbolNoAntiquot.formatter (sym : String) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.nonReservedSymbolNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter

def Lean.PrettyPrinter.Formatter.rawCh.formatter (ch : Char) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.rawCh.formatter ch = Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter (Char.toString ch)

def Lean.PrettyPrinter.Formatter.unicodeSymbolNoAntiquot.formatter (sym : String) (asciiSym : String) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.identNoAntiquot.formatter:

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.rawIdentNoAntiquot.formatter:

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.identEq.formatter (_id : Lean.Name) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.identEq.formatter _id = Lean.PrettyPrinter.Formatter.rawIdentNoAntiquot.formatter

def Lean.PrettyPrinter.Formatter.visitAtom (k : Lean.SyntaxNodeKind) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.charLitNoAntiquot.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.charLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.charLitKind

def Lean.PrettyPrinter.Formatter.strLitNoAntiquot.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.strLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.strLitKind

def Lean.PrettyPrinter.Formatter.nameLitNoAntiquot.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.nameLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.nameLitKind

def Lean.PrettyPrinter.Formatter.numLitNoAntiquot.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.numLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.numLitKind

def Lean.PrettyPrinter.Formatter.scientificLitNoAntiquot.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.scientificLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.scientificLitKind

def Lean.PrettyPrinter.Formatter.fieldIdx.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.fieldIdx.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.fieldIdxKind

def Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.many1NoAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.many1NoAntiquot.formatter p = Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter p

def Lean.PrettyPrinter.Formatter.optionalNoAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.optionalNoAntiquot.formatter p = Lean.PrettyPrinter.Formatter.visitArgs p

def Lean.PrettyPrinter.Formatter.many1Unbox.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.sepByNoAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) (pSep : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.sepBy1NoAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) (pSep : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.sepBy1NoAntiquot.formatter = Lean.PrettyPrinter.Formatter.sepByNoAntiquot.formatter

def Lean.PrettyPrinter.Formatter.withPosition.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.withPosition.formatter p = p

def Lean.PrettyPrinter.Formatter.withPositionAfterLinebreak.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.withPositionAfterLinebreak.formatter p = p

def Lean.PrettyPrinter.Formatter.withoutPosition.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.withoutPosition.formatter p = p

def Lean.PrettyPrinter.Formatter.withForbidden.formatter (_tk : Lean.Parser.Token) (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.withForbidden.formatter _tk p = p

def Lean.PrettyPrinter.Formatter.withoutForbidden.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.withoutForbidden.formatter p = p

def Lean.PrettyPrinter.Formatter.withoutInfo.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.withoutInfo.formatter p = p

def Lean.PrettyPrinter.Formatter.setExpected.formatter (_expected : List String) (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.setExpected.formatter _expected p = p

def Lean.PrettyPrinter.Formatter.incQuotDepth.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.incQuotDepth.formatter p = p

def Lean.PrettyPrinter.Formatter.decQuotDepth.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.decQuotDepth.formatter p = p

def Lean.PrettyPrinter.Formatter.suppressInsideQuot.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.suppressInsideQuot.formatter p = p

def Lean.PrettyPrinter.Formatter.evalInsideQuot.formatter (_declName : Lean.Name) (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.evalInsideQuot.formatter _declName p = p

def Lean.PrettyPrinter.Formatter.checkWsBefore.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.checkWsBefore.formatter = do let st ← get if (st.leadWord != "") = true then Lean.PrettyPrinter.Formatter.pushLine else pure PUnit.unit

def Lean.PrettyPrinter.Formatter.checkPrec.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.checkPrec.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkLhsPrec.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.checkLhsPrec.formatter = pure ()

def Lean.PrettyPrinter.Formatter.setLhsPrec.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.setLhsPrec.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkStackTop.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.checkStackTop.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkNoWsBefore.formatter:

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.checkLinebreakBefore.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.checkLinebreakBefore.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkTailWs.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.checkTailWs.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkColGe.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.checkColGe.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkColGt.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.checkColGt.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkLineEq.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.checkLineEq.formatter = pure ()

def Lean.PrettyPrinter.Formatter.eoi.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.eoi.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkNoImmediateColon.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.checkNoImmediateColon.formatter = pure ()

def Lean.PrettyPrinter.Formatter.skip.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.skip.formatter = pure ()

def Lean.PrettyPrinter.Formatter.pushNone.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.pushNone.formatter = Lean.Syntax.MonadTraverser.goLeft

def Lean.PrettyPrinter.Formatter.withOpenDecl.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.withOpenDecl.formatter p = p

def Lean.PrettyPrinter.Formatter.withOpen.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.withOpen.formatter p = p

def Lean.PrettyPrinter.Formatter.interpolatedStr.formatter (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.dbgTraceState.formatter (_label : String) (p : Lean.PrettyPrinter.Formatter) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.dbgTraceState.formatter _label p = p

@[macroInline]

def Lean.PrettyPrinter.Formatter.ite:

{x : Type} → (c : Prop) → [inst : Decidable c] → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.ite c t e = if c then t else e

@[inline]

abbrev Lean.PrettyPrinter.Formatter.FormatterAliasValue:

Type

Equations

Lean.PrettyPrinter.Formatter.FormatterAliasValue = Lean.Parser.AliasValue Lean.PrettyPrinter.Formatter

opaque Lean.PrettyPrinter.Formatter.formatterAliasesRef:

IO.Ref (Lean.NameMap Lean.PrettyPrinter.Formatter.FormatterAliasValue)

def Lean.PrettyPrinter.Formatter.registerAlias (aliasName : Lean.Name) (v : Lean.PrettyPrinter.Formatter.FormatterAliasValue) :

Equations

Lean.PrettyPrinter.Formatter.registerAlias aliasName v = Lean.Parser.registerAliasCore Lean.PrettyPrinter.Formatter.formatterAliasesRef aliasName v

instance Lean.PrettyPrinter.Formatter.instCoeFormatterFormatterAliasValue:

Coe Lean.PrettyPrinter.Formatter Lean.PrettyPrinter.Formatter.FormatterAliasValue

Equations

Lean.PrettyPrinter.Formatter.instCoeFormatterFormatterAliasValue = { coe := Lean.Parser.AliasValue.const }

instance Lean.PrettyPrinter.Formatter.instCoeForAllFormatterFormatterAliasValue:

Coe (Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter) Lean.PrettyPrinter.Formatter.FormatterAliasValue

Equations

Lean.PrettyPrinter.Formatter.instCoeForAllFormatterFormatterAliasValue = { coe := Lean.Parser.AliasValue.unary }

instance Lean.PrettyPrinter.Formatter.instCoeForAllFormatterFormatterAliasValue_1:

Coe (Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter) Lean.PrettyPrinter.Formatter.FormatterAliasValue

Equations

Lean.PrettyPrinter.Formatter.instCoeForAllFormatterFormatterAliasValue_1 = { coe := Lean.Parser.AliasValue.binary }

def Lean.PrettyPrinter.format (formatter : Lean.PrettyPrinter.Formatter) (stx : Lean.Syntax) :

Lean.CoreM Lean.Format

Equations

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

def Lean.PrettyPrinter.formatCategory (cat : Lean.Name) (stx : Lean.Syntax) :

Lean.CoreM Lean.Format

Equations

Lean.PrettyPrinter.formatCategory cat = Lean.PrettyPrinter.format (Lean.PrettyPrinter.Formatter.categoryFormatter cat)

def Lean.PrettyPrinter.formatTerm (stx : Lean.Syntax) :

Lean.CoreM Lean.Format

Equations

Lean.PrettyPrinter.formatTerm = Lean.PrettyPrinter.formatCategory `term

def Lean.PrettyPrinter.formatTactic (stx : Lean.Syntax) :

Lean.CoreM Lean.Format

Equations

Lean.PrettyPrinter.formatTactic = Lean.PrettyPrinter.formatCategory `tactic

def Lean.PrettyPrinter.formatCommand (stx : Lean.Syntax) :

Lean.CoreM Lean.Format

Equations

Lean.PrettyPrinter.formatCommand = Lean.PrettyPrinter.formatCategory `command