def Lean.PrettyPrinter.Delaborator.withTypeAscription (d : Delab) (cond : Bool := true) : Delab

If cond is true, wraps the syntax produced by d in a type ascription.

def Lean.PrettyPrinter.Delaborator.maybeAddBlockImplicit (identLike : Syntax) : DelabM Syntax

Wraps the identifier (or identifier with explicit universe levels) with @ if pp.analysis.blockImplicit is set to true.

def Lean.PrettyPrinter.Delaborator.delabFVar : Delab

def Lean.PrettyPrinter.Delaborator.delabBVar : Delab

def Lean.PrettyPrinter.Delaborator.delabMVarAux (m : MVarId) : DelabM Term

def Lean.PrettyPrinter.Delaborator.delabMVar : Delab

def Lean.PrettyPrinter.Delaborator.delabSort : Delab

def Lean.PrettyPrinter.Delaborator.delabConst : Delab

Delaborator for const expressions. This is not registered as a delaborator, as const is not an expression kind (see [delab] description and Lean.PrettyPrinter.Delaborator.getExprKind). Rather, it is called through the app delaborator.

def Lean.PrettyPrinter.Delaborator.withFnRefWhenTagAppFns (d : Delab) : Delab

If pp.tagAppFns is set, and if the current expression is a constant application, then d is evaluated with the head constant delaborated with delabConst as the ref.

def Lean.PrettyPrinter.Delaborator.withMDataOptions {α : Type} [Inhabited α] (x : DelabM α) : DelabM α

partial def Lean.PrettyPrinter.Delaborator.withMDatasOptions {α : Type} [Inhabited α] (x : DelabM α) : DelabM α

structure Lean.PrettyPrinter.Delaborator.ParamKind : Type

A structure that records details of a function parameter.

• name : Name

  Binder name for the parameter.

• bInfo : BinderInfo

  Binder info for the parameter.

• defVal : Option Expr

  The default value for the parameter, if the parameter has a default value.

• isAutoParam : Bool

  Whether the parameter is an autoparam (i.e., whether it uses a tactic for the default value).

instance Lean.PrettyPrinter.Delaborator.instInhabitedParamKind : Inhabited ParamKind

def Lean.PrettyPrinter.Delaborator.ParamKind.isRegularExplicit (param : ParamKind) : Bool

Returns true if the parameter is an explicit parameter that has neither a default value nor a tactic.

def Lean.PrettyPrinter.Delaborator.getParamKinds (f : Expr) (args : Array Expr) : MetaM (Array ParamKind)

Given a function f supplied with arguments args, returns an array whose n-th element is set to the kind of the n-th argument's associated parameter. We do not assume the expression mkAppN f args is sensical, and this function captures errors (except for panics) and returns the empty array in that case.

The returned array might be longer than the number of arguments. It gives parameter kinds for the fully-applied function. Note: the defVal expressions are only guaranteed to be valid for parameters associated to the supplied arguments; after this, they might refer to temporary fvars.

This function properly handles "overapplied" functions. For example, while id takes one explicit argument, it can take more than one explicit argument when its arguments are specialized to function types, like in id id 2.

def Lean.PrettyPrinter.Delaborator.shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool

def Lean.PrettyPrinter.Delaborator.appFieldNotationCandidate? : DelabM (Option (Nat × Name))

If e is an application that is a candidate for using field notation, returns the parameter index and the field name to use. Checks that there are enough arguments.

def Lean.PrettyPrinter.Delaborator.needsExplicit (f : Expr) (numArgs : Nat) (paramKinds : Array ParamKind) : Bool

In explicit mode, decides whether or not the applied function needs @, where numArgs is the number of arguments actually supplied to f.

def Lean.PrettyPrinter.Delaborator.delabAppExplicitCore (fieldNotation : Bool) (numArgs : Nat) (delabHead : Bool → Delab) (paramKinds : Array ParamKind) : Delab

Delaborates a function application in explicit mode.

• If insertExplicit is true, then ensures the head syntax is wrapped with @.
• If fieldNotation is true, then allows the application to be pretty printed using field notation. Field notation will not be used when insertExplicit is true.

inductive Lean.PrettyPrinter.Delaborator.AppImplicitArg : Type

Records how a particular argument to a function is delaborated, in non-explicit mode.

• skip : AppImplicitArg

  An argument to skip, like an implicit argument.

• regular (s : Term) : AppImplicitArg

  A regular argument.

• optional (name : Name) (s : Term) : AppImplicitArg

  A regular argument that, if it comes as the last argument, may be omitted.

• named (s : TSyntax `Lean.Parser.Term.namedArgument) : AppImplicitArg

  It's a named argument. Named arguments inhibit applying unexpanders.

instance Lean.PrettyPrinter.Delaborator.instInhabitedAppImplicitArg : Inhabited AppImplicitArg

def Lean.PrettyPrinter.Delaborator.AppImplicitArg.canUnexpand : AppImplicitArg → Bool

Whether unexpanding is allowed with this argument.

def Lean.PrettyPrinter.Delaborator.AppImplicitArg.syntax? : AppImplicitArg → Option Syntax

If the argument has associated syntax, returns it.

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) : Delab

Delaborates a function application in the standard mode, where implicit arguments are generally not included, unless pp.analysis.namedArg is set at that argument.

This delaborator is where app_unexpanders and the structure instance unexpander are applied, if unexpand is true. When unexpand is true, also considers opportunities for field notation, which takes priority over other unexpanders.

Assumes numArgs ≤ paramKinds.size.

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.mkNamedArg (name : Name) : DelabM AppImplicitArg

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.mkArg (isFieldIdx : Bool) (param : ParamKind) : DelabM AppImplicitArg

Delaborates the current argument. The argument remainingArgs is the number of arguments in the application after this one.

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.tryUnexpand (ref : Syntax) (fs : List Unexpander) (stx : Syntax) : DelabM Syntax

Runs the given unexpanders, returning the resulting syntax if any are applicable, and otherwise fails.

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.tryAppUnexpanders (fnStx : Term) (args : Array AppImplicitArg) : Delab

If the expression is a candidate for app unexpanders, try applying an app unexpander using some prefix of the arguments, longest prefix first. This function makes sure that the unexpanded syntax is annotated and given TermInfo so that it is hoverable in the InfoView.

Ref logic:

1. The unexpanders are run with the head constant's syntax as the ref.
2. If pp.tagAppFns is false, then this does nothing, since delabConst won't register any terminfo for the constant.
3. If pp.tagAppFns is true, then this causes all tokens in app unexpanders to refer to the head constant. The effect is that in docgen, every token will be linkified (supposing the app unexpander uses syntax quotations).

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.tryAppUnexpanders.go (fnStx : Term) (args : Array AppImplicitArg) (fs : List Unexpander) (i implicitArgs : Nat) (argStxs : Array Syntax) : DelabM Term

def Lean.PrettyPrinter.Delaborator.useAppExplicit (numArgs : Nat) (paramKinds : Array ParamKind) : DelabM Bool

Returns true if an application should use explicit mode when delaborating. Explicit mode turns off unexpanders

def Lean.PrettyPrinter.Delaborator.delabAppCore (maxArgs : Nat) (delabHead : Bool → Delab) (unexpand : Bool) : Delab

Delaborates applications. Removes up to maxArgs arguments to form the "head" of the application.

• delabHead is a delaborator to use for the head of the expression. It is passed whether the result needs to have @ inserted.
• If unexpand is true, then allow unexpanders and field notation. This should likely be set to false except in the main delabApp delaborator.

Propagates pp.tagAppFns into the head for delabHead.

def Lean.PrettyPrinter.Delaborator.delabApp : Delab

Default delaborator for applications.

def Lean.PrettyPrinter.Delaborator.withOverApp (arity : Nat) (x : Delab) : Delab

The withOverApp combinator allows delaborators to handle "over-application" by using the core application delaborator to handle additional arguments.

For example, suppose f : {A : Type} → Foo A → A and we want to implement a delaborator for applications f x to pretty print as F[x]. Because A is a type variable we might encounter a term of the form @f (A → B) x y, which has an additional argument y. With this combinator one can use an arity-2 delaborator to pretty print this as F[x] y.

• arity: the expected number of arguments to f. The combinator will fail if fewer than this number of arguments are passed, and if more than this number of arguments are passed the arguments are handled using the standard application delaborator.
• x: delaborates the head application of the expected arity (f x in the example). The value of pp.tagAppFns for the whole application is propagated to the expression that x sees.

In the event of overapplication, the delaborator x is wrapped in Lean.PrettyPrinter.Delaborator.withAnnotateTermInfo to register TermInfo for the resulting term. The effect of this is that the term is hoverable in the Infoview.

If the application would require inserting @ around the result of x, the delaborator fails since we cannot be sure that this insertion will be well-formed.

def Lean.PrettyPrinter.Delaborator.delabDelayedAssignedMVar : Delab

def Lean.PrettyPrinter.Delaborator.delabStructureInstance : Delab

Delaborate structure constructor applications using structure instance notation or anonymous constructor notation.

structure Lean.PrettyPrinter.Delaborator.AppMatchState : Type

State for delabAppMatch and helpers.

• info : Meta.MatcherInfo
• matcherTy : SubExpr

  The matcherTy instantiated with universe levels and the matcher parameters, with a position at the type of this application prefix.

• motive : Option (Term × Expr)

  The motive, with the pi type version delaborated and the original expression version. Once AppMatchState is complete, this is not none.

• motiveNamed : Bool

  Whether pp.analysis.namedArg was set for the motive argument.

• discrs : Array Term

  The delaborated discriminants, without h : annotations.

• hNames? : Array (Option Name)

  The collection of names used for the h : discriminant annotations, in order. Uniquified names are constructed after the first phase.

• alts : Array SubExpr

  Lambda subexpressions for each alternate.

• varNames : Array (Array Name)

  For each match alternative, the names to use for the pattern variables. Each ends with hNames?.filterMap id exactly.

• rhss : Array Term

  The delaborated right-hand sides for each match alternative.

def Lean.PrettyPrinter.Delaborator.delabAppMatch : Delab

Delaborates applications of "matchers" such as

List.map.match_1 : {α : Type _} →
  (motive : List α → Sort _) →
    (x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x

partial def Lean.PrettyPrinter.Delaborator.delabAppMatch.withDummyBinders {α : Type} (hNames? : Array (Option Name)) (body : Expr) (m : Array (Option Name) → DelabM α) (acc : Array (Option Name) := #[]) : DelabM α

Adds hNames to the local context to reserve their names and runs m in that context.

partial def Lean.PrettyPrinter.Delaborator.delabAppMatch.usingNames {α : Type} (varNames : Array Name) (x : DelabM α) (i : Nat := 0) : DelabM α

def Lean.PrettyPrinter.Delaborator.delabLetFun : Delab

Delaborates applications of the form letFun v (fun x => b) as have x := v; b.

def Lean.PrettyPrinter.Delaborator.delabMData : Delab

def Lean.PrettyPrinter.Delaborator.delabLam : Delab

def Lean.PrettyPrinter.Delaborator.delabForall : Delab

def Lean.PrettyPrinter.Delaborator.delabLetE : Delab

def Lean.PrettyPrinter.Delaborator.delabChar : Delab

def Lean.PrettyPrinter.Delaborator.delabLit : Delab

def Lean.PrettyPrinter.Delaborator.delabOfNatCore (showType : Bool := false) : Delab

Core function that delaborates a natural number (an OfNat.ofNat literal).

def Lean.PrettyPrinter.Delaborator.delabNegIntCore (showType : Bool := false) : Delab

Core function that delaborates a negative integer literal (a Neg.neg applied to OfNat.ofNat).

def Lean.PrettyPrinter.Delaborator.delabDivRatCore (showType : Bool := false) : Delab

Core function that delaborates a rational literal that is the division of an integer literal by a natural number literal. The division must be homogeneous for it to count as a rational literal.

def Lean.PrettyPrinter.Delaborator.delabOfNat : Delab

Delaborates an OfNat.ofNat literal. @OfNat.ofNat _ n _ ~> n.

def Lean.PrettyPrinter.Delaborator.delabNeg : Delab

Delaborates the negative of an OfNat.ofNat literal. -@OfNat.ofNat _ n _ ~> -n

def Lean.PrettyPrinter.Delaborator.delabHDiv : Delab

Delaborates a rational number literal. @OfNat.ofNat _ n _ / @OfNat.ofNat _ m ~> n / m and -@OfNat.ofNat _ n _ / @OfNat.ofNat _ m ~> -n / m

def Lean.PrettyPrinter.Delaborator.delabOfScientific : Delab

def Lean.PrettyPrinter.Delaborator.delabProj : Delab

Delaborate a projection primitive. These do not usually occur in user code, but are pretty-printed when e.g. #printing a projection function.

def Lean.PrettyPrinter.Delaborator.coeDelaborator : Delab

This delaborator tries to elide functions which are known coercions. For example, Int.ofNat is a coercion, so instead of printing ofNat n we just print ↑n, and when re-parsing this we can (usually) recover the specific coercion being used.

def Lean.PrettyPrinter.Delaborator.coeDelaborator.delabHead (info : Meta.CoeFnInfo) (nargs : Nat) (insertExplicit : Bool) : Delab

def Lean.PrettyPrinter.Delaborator.delabDIte : Delab

def Lean.PrettyPrinter.Delaborator.delabDIte.delabBranch (h? : Option Name) : DelabM (Syntax × Name)

def Lean.PrettyPrinter.Delaborator.delabCond : Delab

def Lean.PrettyPrinter.Delaborator.delabNamedPattern : Delab

def Lean.PrettyPrinter.Delaborator.delabSigmaCore (sigma : Bool) : Delab

def Lean.PrettyPrinter.Delaborator.delabSigma : Delab

def Lean.PrettyPrinter.Delaborator.delabPSigma : Delab

def Lean.PrettyPrinter.Delaborator.delabPProdMkCore (mkName : Name) : Delab

def Lean.PrettyPrinter.Delaborator.delabPProdMk : Delab

def Lean.PrettyPrinter.Delaborator.delabMProdMk : Delab

partial def Lean.PrettyPrinter.Delaborator.delabDoElems : DelabM (List Syntax)

partial def Lean.PrettyPrinter.Delaborator.delabDoElems.prependAndRec (x : DelabM Syntax) : DelabM (List Syntax)

def Lean.PrettyPrinter.Delaborator.delabDo : Delab

def Lean.PrettyPrinter.Delaborator.delabLazyBinop (arity : Nat) (k : Term → Term → DelabM Term) : DelabM Term

Delaborates a function application of the form f ... x (fun _ : Unit => y).

def Lean.PrettyPrinter.Delaborator.delabHOrElse : Delab

def Lean.PrettyPrinter.Delaborator.delabHAndThen : Delab

def Lean.PrettyPrinter.Delaborator.delabSeq : Delab

def Lean.PrettyPrinter.Delaborator.delabSeqLeft : Delab

def Lean.PrettyPrinter.Delaborator.delabSeqRight : Delab

def Lean.PrettyPrinter.Delaborator.delabNameMkStr : Delab

def Lean.PrettyPrinter.Delaborator.delabNameMkNum : Delab

def Lean.PrettyPrinter.Delaborator.delabSorry : Delab

def Lean.PrettyPrinter.Delaborator.declSigWithId : Parser.Parser

def Lean.PrettyPrinter.Delaborator.delabConstWithSignature (universes : Bool := true) : Delab

Pretty-prints a constant c as c.{<levels>} <params> : <type>.

If universes is false, then the universe level parameters are omitted.

def Lean.PrettyPrinter.Delaborator.delabConstWithSignature.delabTy : DelabM Term

For types in the signature, we want to be sure pi binder types are pretty printed.

partial def Lean.PrettyPrinter.Delaborator.delabConstWithSignature.delabParams (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray `Lean.Parser.Term.bracketedBinder) : DelabM Term

partial def Lean.PrettyPrinter.Delaborator.delabConstWithSignature.delabParamsAux (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray `Lean.Parser.Term.bracketedBinder) (curIds : Array Ident) : DelabM Term

Inner loop for delabParams, collecting binders. Invariants:

• The current expression is a forall.
• It has a name that's not inaccessible.
• It has a name that hasn't been used yet.

def Lean.PrettyPrinter.Delaborator.delabConstWithSignature.shouldGroupWithNext (bindingNames : NameSet) (e e' : Expr) : Bool

partial def Lean.PrettyPrinter.Delaborator.delabConstWithSignature.processSpine (opts : OptionsPerPos) (subExpr : SubExpr) : MetaM (OptionsPerPos × Expr)

Go through rest of type, alpha renaming and setting options along the spine.