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

Equations

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

def Lean.PrettyPrinter.Delaborator.unfoldMDatas : Lean.Expr → Lean.Expr

Equations

• Lean.PrettyPrinter.Delaborator.unfoldMDatas (Lean.Expr.mdata data e) = Lean.PrettyPrinter.Delaborator.unfoldMDatas e
• Lean.PrettyPrinter.Delaborator.unfoldMDatas x = x

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

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 α

def Lean.PrettyPrinter.Delaborator.delabAppFn : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

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

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.

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.useAppExplicit (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.isRegularApp (maxArgs : Nat) : Lean.PrettyPrinter.Delaborator.DelabM Bool

Returns true if the application is a candidate for unexpanders.

Equations

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

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

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.delabAppExplicitCore (maxArgs : Nat) (delabHead : Lean.PrettyPrinter.Delaborator.Delab) (paramKinds : Array Lean.PrettyPrinter.Delaborator.ParamKind) (tagAppFn : Bool) : Lean.PrettyPrinter.Delaborator.Delab

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

Equations

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

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

Delaborates a function application in the standard mode, where implicit arguments are generally not included.

Equations

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

def Lean.PrettyPrinter.Delaborator.delabAppCore (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. The remaining arguments are processed depending on whether heuristics indicate that the application should be delaborated using @.

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: constructs data corresponding to the main application (f x in the example)

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

Delaborate a call to a projection function such as Prod.fst.

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