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

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

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

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

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

def Lean.PrettyPrinter.Delaborator.delabConst : Lean.PrettyPrinter.Delaborator.Delab

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

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

structure Lean.PrettyPrinter.Delaborator.ParamKind : Type

• name : Lake.Name
• bInfo : Lean.BinderInfo
• defVal : Option Lean.Expr
• isAutoParam : Bool

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

def Lean.PrettyPrinter.Delaborator.getParamKinds : Lean.PrettyPrinter.Delaborator.DelabM (Array Lean.PrettyPrinter.Delaborator.ParamKind)

Return array with n-th element set to kind of n-th parameter of e.

partial def Lean.PrettyPrinter.Delaborator.getParamKinds.forallTelescopeArgs (f : Lean.Expr) (args : Array Lean.Expr) (k : Array Lean.Expr → Lean.Expr → Lean.PrettyPrinter.Delaborator.DelabM (Array Lean.PrettyPrinter.Delaborator.ParamKind)) : Lean.PrettyPrinter.Delaborator.DelabM (Array Lean.PrettyPrinter.Delaborator.ParamKind)

def Lean.PrettyPrinter.Delaborator.delabAppExplicit : Lean.PrettyPrinter.Delaborator.Delab

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

def Lean.PrettyPrinter.Delaborator.isRegularApp : Lean.PrettyPrinter.Delaborator.DelabM Bool

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

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

def Lean.PrettyPrinter.Delaborator.delabAppImplicit : Lean.PrettyPrinter.Delaborator.Delab

structure Lean.PrettyPrinter.Delaborator.AppMatchState : Type

• 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

State for delabAppMatch and helpers.

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Pretty-prints a constant c as c.{} : .

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