Documentation

Lean.PrettyPrinter.Delaborator.Builtins

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 a e a_1) = Lean.PrettyPrinter.Delaborator.unfoldMDatas e
Lean.PrettyPrinter.Delaborator.unfoldMDatas _fun_discr = _fun_discr

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.unresolveNameGlobal (n₀ : Lean.Name) :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Name

Equations

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

def Lean.PrettyPrinter.Delaborator.unresolveNameGlobal.unresolveNameCore (n₀ : Lean.Name) (n : Lean.Name) :

Lean.PrettyPrinter.Delaborator.DelabM (Option Lean.Name)

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} [inst : 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} [inst : 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

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

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

Equations

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

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.

Equations

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

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

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

Lean.PrettyPrinter.Delaborator.DelabM Bool

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.unexpandCoe (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.delabAppImplicit:

Lean.PrettyPrinter.Delaborator.Delab

Equations

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

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

Equations

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

def Lean.PrettyPrinter.Delaborator.delabLetFun:

Lean.PrettyPrinter.Delaborator.Delab

Delaborate applications of the form (fun x => b) v 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 : Lean.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.delabOfNat:

Lean.PrettyPrinter.Delaborator.Delab

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 Lean.Name) :

Lean.PrettyPrinter.Delaborator.DelabM (Lean.Syntax × Lean.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 Lean.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