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

• param.isRegularExplicit = (param.bInfo.isExplicit && !param.isAutoParam && param.defVal.isNone)

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

Takes application syntax and converts it into structure instance notation, if possible. Assumes that the application is pretty printed in implicit mode.

Equations

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

def Lean.PrettyPrinter.Delaborator.appFieldNotationCandidate? : Lean.PrettyPrinter.Delaborator.DelabM (Option (Nat × Lake.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.

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

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

Equations

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

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

Equations

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

inductive Lean.PrettyPrinter.Delaborator.AppImplicitArg : Type

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

• skip: Lean.PrettyPrinter.Delaborator.AppImplicitArg

  An argument to skip, like an implicit argument.

• regular: Lean.Term → Lean.PrettyPrinter.Delaborator.AppImplicitArg

  A regular argument.

• named: Lean.TSyntax `Lean.Parser.Term.namedArgument → Lean.PrettyPrinter.Delaborator.AppImplicitArg

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

instance Lean.PrettyPrinter.Delaborator.instInhabitedAppImplicitArg : Inhabited Lean.PrettyPrinter.Delaborator.AppImplicitArg

Equations

• Lean.PrettyPrinter.Delaborator.instInhabitedAppImplicitArg = { default := Lean.PrettyPrinter.Delaborator.AppImplicitArg.skip }

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

Whether unexpanding is allowed with this argument.

Equations

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

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

If the argument has associated syntax, returns it.

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, if unexpand is true. When unexpand is true, also considers opportunities for field notation, which takes priority over other unexpanders.

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) : Lean.PrettyPrinter.Delaborator.DelabM Lean.PrettyPrinter.Delaborator.AppImplicitArg

Equations

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

def Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.mkArg (remainingArgs : Nat) (param : Lean.PrettyPrinter.Delaborator.ParamKind) : Lean.PrettyPrinter.Delaborator.DelabM Lean.PrettyPrinter.Delaborator.AppImplicitArg

Delaborates the current argument. The argument 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) (args : Array Lean.PrettyPrinter.Delaborator.AppImplicitArg) : 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) (args : Array Lean.PrettyPrinter.Delaborator.AppImplicitArg) (fs : List Lean.PrettyPrinter.Unexpander) (i : Nat) (implicitArgs : Nat) (argStxs : Array Lean.Syntax) : 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. Explicit mode turns off unexpanders

Equations

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

def Lean.PrettyPrinter.Delaborator.delabAppCore (maxArgs : Nat) (delabHead : Bool → Lean.PrettyPrinter.Delaborator.Delab) (unexpand : Bool) : Lean.PrettyPrinter.Delaborator.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.

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.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: 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.

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.SubExpr

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

• motive : Option (Lean.Term × Lean.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 Lean.Term

  The delaborated discriminants, without h : annotations.

• hNames? : Array (Option Lake.Name)

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

• alts : Array Lean.SubExpr

  Lambda subexpressions for each alternate.

• varNames : Array (Array Lake.Name)

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

• rhss : Array Lean.Term

  The delaborated right-hand sides for each match alternative.

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

Equations

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

partial def Lean.PrettyPrinter.Delaborator.delabAppMatch.withDummyBinders {α : Type} (hNames? : Array (Option Lake.Name)) (body : Lean.Expr) (m : Array (Option Lake.Name) → Lean.PrettyPrinter.Delaborator.DelabM α) (acc : optParam (Array (Option Lake.Name)) #[]) : Lean.PrettyPrinter.Delaborator.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 Lake.Name) (x : Lean.PrettyPrinter.Delaborator.DelabM α) (i : optParam Nat 0) : Lean.PrettyPrinter.Delaborator.DelabM α

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.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 (universes : optParam Bool true) : Lean.PrettyPrinter.Delaborator.Delab

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

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

Equations

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

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

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

Equations

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

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

partial def Lean.PrettyPrinter.Delaborator.delabConstWithSignature.delabParamsAux (bindingNames : Lean.NameSet) (idStx : Lean.Ident) (groups : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) (curIds : Array Lean.Ident) : Lean.PrettyPrinter.Delaborator.DelabM Lean.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 : Lean.NameSet) (e : Lean.Expr) (e' : Lean.Expr) : Bool

Equations

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