def Lean.PrettyPrinter.Delaborator.withTypeAscription (d : Lean.PrettyPrinter.Delaborator.Delab) (cond : optParam Bool true) : Lean.PrettyPrinter.Delaborator.DelabM Lean.Term

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

Equations

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

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

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabFVar : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabBVar : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabMVar : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabSort : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabConst : Lean.PrettyPrinter.Delaborator.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.

Equations

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

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

Equations

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

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

structure Lean.PrettyPrinter.Delaborator.ParamKind : Type

A structure that records details of a function parameter.

• name : Lake.Name

  Binder name for the parameter.

• bInfo : Lean.BinderInfo

  Binder info for the parameter.

• defVal : Option Lean.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 Lean.PrettyPrinter.Delaborator.ParamKind

Equations

• Lean.PrettyPrinter.Delaborator.instInhabitedParamKind = { default := { name := default, bInfo := default, defVal := default, isAutoParam := default } }

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

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

Equations

• Lean.PrettyPrinter.Delaborator.ParamKind.isRegularExplicit param = (Lean.BinderInfo.isExplicit param.bInfo && !param.isAutoParam && Option.isNone param.defVal)

def Lean.PrettyPrinter.Delaborator.getParamKinds (f : Lean.Expr) (args : Array Lean.Expr) : Lean.MetaM (Array Lean.PrettyPrinter.Delaborator.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.

Equations

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

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

Equations

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

def Lean.PrettyPrinter.Delaborator.unexpandStructureInstance (stx : Lean.Syntax) : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

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

Given an application of numArgs arguments with the calculated ParamKinds, returns true if we should wrap the applied function with @ when we are in explicit mode.

Equations

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

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

Delaborates a function application in explicit mode, and ensures the resulting head syntax is wrapped with @ if needed.

Equations

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

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Lean.PrettyPrinter.Delaborator.Delab) (paramKinds : Array Lean.PrettyPrinter.Delaborator.ParamKind) : Lean.PrettyPrinter.Delaborator.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.

Assumes numArgs ≤ paramKinds.size.

Equations

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

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.mkNamedArg (name : Lake.Name) (argStx : Lean.Syntax) : Lean.PrettyPrinter.Delaborator.DelabM (Bool × Option Lean.Syntax)

Equations

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

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.mkArgStx (remainingArgs : Nat) (paramKinds : List Lean.PrettyPrinter.Delaborator.ParamKind) : Lean.PrettyPrinter.Delaborator.DelabM (Bool × Option Lean.Syntax)

If the argument should be pretty printed then it returns the syntax for that argument. The boolean is false if an unexpander should not be used for the application due to this argument. The argumnet remainingArgs is the number of arguments in the application after this one.

Equations

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

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

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.tryAppUnexpanders (fnStx : Lean.Term) (argStxs : Array Lean.Syntax) (argData : Array (Bool × Nat)) : Lean.PrettyPrinter.Delaborator.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.

Equations

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

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.tryAppUnexpanders.go (fnStx : Lean.Term) (argStxs : Array Lean.Syntax) (argData : Array (Bool × Nat)) (fs : List Lean.PrettyPrinter.Unexpander) (prefixArgs : Nat) : Lean.PrettyPrinter.Delaborator.DelabM Lean.Term

Equations

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

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

Returns true if an application should use explicit mode when delaborating.

Equations

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

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

Delaborates applications. Removes up to maxArgs arguments to form the "head" of the application and delaborates the head using delabHead. Then the application is then processed in explicit mode or implicit mode depending on which should be used.

Equations

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

def Lean.PrettyPrinter.Delaborator.delabApp : Lean.PrettyPrinter.Delaborator.Delab

Default delaborator for applications.

Equations

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

def Lean.PrettyPrinter.Delaborator.delabApp.delabAppFn (tagAppFn : Bool) : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.withOverApp (arity : Nat) (x : Lean.PrettyPrinter.Delaborator.Delab) : Lean.PrettyPrinter.Delaborator.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: constructs data corresponding to the main application (f x in the example).

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.

Equations

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

structure Lean.PrettyPrinter.Delaborator.AppMatchState : Type

State for delabAppMatch and helpers.

• info : Lean.Meta.MatcherInfo
• matcherTy : Lean.Expr
• params : Array Lean.Expr
• motive : Option (Lean.Term × Lean.Expr)
• motiveNamed : Bool
• discrs : Array Lean.Term
• varNames : Array (Array Lake.Name)
• rhss : Array Lean.Term
• moreArgs : Array Lean.Term

def Lean.PrettyPrinter.Delaborator.delabAppMatch : Lean.PrettyPrinter.Delaborator.Delab

Delaborate 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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabLetFun : Lean.PrettyPrinter.Delaborator.Delab

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabMData : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

partial def Lean.PrettyPrinter.Delaborator.hasIdent (id : Lake.Name) : Lean.Syntax → Bool

Check for a Syntax.ident of the given name anywhere in the tree. This is usually a bad idea since it does not check for shadowing bindings, but in the delaborator we assume that bindings are never shadowed.

def Lean.PrettyPrinter.Delaborator.delabLam : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabForall : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabLetE : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabChar : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabLit : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

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

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

Equations

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

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

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabDivRatCore (showType : optParam Bool false) : Lean.PrettyPrinter.Delaborator.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.

Equations

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

def Lean.PrettyPrinter.Delaborator.delabOfNat : Lean.PrettyPrinter.Delaborator.Delab

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabNeg : Lean.PrettyPrinter.Delaborator.Delab

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabHDiv : Lean.PrettyPrinter.Delaborator.Delab

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabOfScientific : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabProj : Lean.PrettyPrinter.Delaborator.Delab

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabProjectionApp : Lean.PrettyPrinter.Delaborator.Delab

Delaborates an application of a projection function, for example Prod.fst p as p.fst. Collapses intermediate parent projections, so for example rather than o.toB.toA.x it produces o.x.

Does not delaborate projection functions from classes, since the instance parameter is implicit; we would rather see default than instInhabitedNat.default.

Equations

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

def Lean.PrettyPrinter.Delaborator.delabProjectionApp.projInfo : Lean.PrettyPrinter.Delaborator.DelabM (Lake.Name × Nat × Bool)

If this is a projection that could delaborate using dot notation, returns the field name, the arity of the projector, and whether this is a parent projection. Otherwise it fails.

Equations

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

partial def Lean.PrettyPrinter.Delaborator.delabProjectionApp.withoutParentProjections {α : Type} (d : Lean.PrettyPrinter.Delaborator.DelabM α) : Lean.PrettyPrinter.Delaborator.DelabM α

Consumes projections to parent structures. For example, if the current expression is o.toB.toA, runs d with o as the current expression.

def Lean.PrettyPrinter.Delaborator.coeDelaborator : Lean.PrettyPrinter.Delaborator.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.

Equations

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

def Lean.PrettyPrinter.Delaborator.delabDIte : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabCond : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabNamedPattern : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabSigma : Lean.PrettyPrinter.Delaborator.Delab

Equations

• Lean.PrettyPrinter.Delaborator.delabSigma = Lean.PrettyPrinter.Delaborator.delabSigmaCore true

def Lean.PrettyPrinter.Delaborator.delabPSigma : Lean.PrettyPrinter.Delaborator.Delab

Equations

• Lean.PrettyPrinter.Delaborator.delabPSigma = Lean.PrettyPrinter.Delaborator.delabSigmaCore false

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

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

def Lean.PrettyPrinter.Delaborator.delabDo : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.reifyName : Lean.Expr → Lean.PrettyPrinter.Delaborator.DelabM Lake.Name

def Lean.PrettyPrinter.Delaborator.delabNameMkStr : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def Lean.PrettyPrinter.Delaborator.delabNameMkNum : Lean.PrettyPrinter.Delaborator.Delab

Equations

• Lean.PrettyPrinter.Delaborator.delabNameMkNum = Lean.PrettyPrinter.Delaborator.delabNameMkStr

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabConstWithSignature : Lean.PrettyPrinter.Delaborator.Delab

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

Equations

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

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