Lean.PrettyPrinter.Delaborator.Builtins

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.

source

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.

source

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

Lean.PrettyPrinter.Delaborator.DelabM α

source

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

Instances For

Lean.PrettyPrinter.Delaborator.instInhabitedParamKind

source

instance Lean.PrettyPrinter.Delaborator.instInhabitedParamKind :

Inhabited Lean.PrettyPrinter.Delaborator.ParamKind

Equations

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

source

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)

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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

source

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.

source

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.

source

def Lean.PrettyPrinter.Delaborator.delabMData :

Lean.PrettyPrinter.Delaborator.Delab

Equations

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

source

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.

source

def Lean.PrettyPrinter.Delaborator.delabLam :

Lean.PrettyPrinter.Delaborator.Delab

Equations

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

source

def Lean.PrettyPrinter.Delaborator.delabForall :

Lean.PrettyPrinter.Delaborator.Delab

Equations

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

source

def Lean.PrettyPrinter.Delaborator.delabLetE :

Lean.PrettyPrinter.Delaborator.Delab

Equations

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

source

def Lean.PrettyPrinter.Delaborator.delabChar :

Lean.PrettyPrinter.Delaborator.Delab

Equations

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

source

def Lean.PrettyPrinter.Delaborator.delabLit :

Lean.PrettyPrinter.Delaborator.Delab

Equations

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

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

def Lean.PrettyPrinter.Delaborator.delabOfScientific :

Lean.PrettyPrinter.Delaborator.Delab

Equations

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

source

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.

source

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.

source

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.

source

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.

source

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