Documentation

Lean.PrettyPrinter.Delaborator.TopDownAnalyze

The top-down analyzer is an optional preprocessor to the delaborator that aims to determine the minimal annotations necessary to ensure that the delaborated expression can be re-elaborated correctly. Currently, the top-down analyzer is neither sound nor complete: there may be edge-cases in which the expression can still not be re-elaborated correctly, and it may also add many annotations that are not strictly necessary.

opaque Lean.pp.analyze :

Lean.Option Bool

opaque Lean.pp.analyze.checkInstances :

Lean.Option Bool

opaque Lean.pp.analyze.typeAscriptions :

Lean.Option Bool

opaque Lean.pp.analyze.trustSubst :

Lean.Option Bool

opaque Lean.pp.analyze.trustOfNat :

Lean.Option Bool

opaque Lean.pp.analyze.trustOfScientific :

Lean.Option Bool

opaque Lean.pp.analyze.trustSubtypeMk :

Lean.Option Bool

opaque Lean.pp.analyze.trustId :

Lean.Option Bool

opaque Lean.pp.analyze.trustKnownFOType2TypeHOFuns :

Lean.Option Bool

opaque Lean.pp.analyze.omitMax :

Lean.Option Bool

opaque Lean.pp.analyze.knowsType :

Lean.Option Bool

opaque Lean.pp.analyze.explicitHoles :

Lean.Option Bool

def Lean.getPPAnalyze (o : Lean.Options) :

Equations

Lean.getPPAnalyze o = Lean.KVMap.get o Lean.pp.analyze.name Lean.pp.analyze.defValue

Instances For

def Lean.getPPAnalyzeCheckInstances (o : Lean.Options) :

Instances For

def Lean.getPPAnalyzeTypeAscriptions (o : Lean.Options) :

Instances For

def Lean.getPPAnalyzeTrustSubst (o : Lean.Options) :

Instances For

def Lean.getPPAnalyzeTrustOfNat (o : Lean.Options) :

Equations

Lean.getPPAnalyzeTrustOfNat o = Lean.KVMap.get o Lean.pp.analyze.trustOfNat.name Lean.pp.analyze.trustOfNat.defValue

Instances For

def Lean.getPPAnalyzeTrustOfScientific (o : Lean.Options) :

Equations

Lean.getPPAnalyzeTrustOfScientific o = Lean.KVMap.get o Lean.pp.analyze.trustOfScientific.name Lean.pp.analyze.trustOfScientific.defValue

Instances For

def Lean.getPPAnalyzeTrustId (o : Lean.Options) :

Equations

Lean.getPPAnalyzeTrustId o = Lean.KVMap.get o Lean.pp.analyze.trustId.name Lean.pp.analyze.trustId.defValue

Instances For

def Lean.getPPAnalyzeTrustSubtypeMk (o : Lean.Options) :

Instances For

def Lean.getPPAnalyzeTrustKnownFOType2TypeHOFuns (o : Lean.Options) :

Equations

Lean.getPPAnalyzeTrustKnownFOType2TypeHOFuns o = Lean.KVMap.get o Lean.pp.analyze.trustKnownFOType2TypeHOFuns.name Lean.pp.analyze.trustKnownFOType2TypeHOFuns.defValue

Instances For

def Lean.getPPAnalyzeOmitMax (o : Lean.Options) :

Equations

Lean.getPPAnalyzeOmitMax o = Lean.KVMap.get o Lean.pp.analyze.omitMax.name Lean.pp.analyze.omitMax.defValue

Instances For

def Lean.getPPAnalyzeKnowsType (o : Lean.Options) :

Equations

Lean.getPPAnalyzeKnowsType o = Lean.KVMap.get o Lean.pp.analyze.knowsType.name Lean.pp.analyze.knowsType.defValue

Instances For

def Lean.getPPAnalyzeExplicitHoles (o : Lean.Options) :

Equations

Lean.getPPAnalyzeExplicitHoles o = Lean.KVMap.get o Lean.pp.analyze.explicitHoles.name Lean.pp.analyze.explicitHoles.defValue

Instances For

def Lean.getPPAnalysisSkip (o : Lean.Options) :

Equations

Lean.getPPAnalysisSkip o = Lean.KVMap.get o `pp.analysis.skip false

Instances For

def Lean.getPPAnalysisHole (o : Lean.Options) :

Equations

Lean.getPPAnalysisHole o = Lean.KVMap.get o `pp.analysis.hole false

Instances For

def Lean.getPPAnalysisNamedArg (o : Lean.Options) :

Instances For

def Lean.getPPAnalysisLetVarType (o : Lean.Options) :

Equations

Lean.getPPAnalysisLetVarType o = Lean.KVMap.get o `pp.analysis.letVarType false

Instances For

def Lean.getPPAnalysisNeedsType (o : Lean.Options) :

Instances For

def Lean.getPPAnalysisBlockImplicit (o : Lean.Options) :

Equations

Lean.getPPAnalysisBlockImplicit o = Lean.KVMap.get o `pp.analysis.blockImplicit false

Instances For

def Lean.getPPAnalysisNoDot (o : Lean.Options) :

Instances For

def Lean.PrettyPrinter.Delaborator.returnsPi (motive : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.PrettyPrinter.Delaborator.returnsPi motive = Lean.Meta.lambdaTelescope motive fun (x : Array Lean.Expr) (b : Lean.Expr) => pure b.isForall

Instances For

def Lean.PrettyPrinter.Delaborator.isNonConstFun (motive : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.PrettyPrinter.Delaborator.isNonConstFun (Lean.Expr.lam binderName binderType b binderInfo) = Lean.PrettyPrinter.Delaborator.isNonConstFun b
Lean.PrettyPrinter.Delaborator.isNonConstFun motive = pure motive.hasLooseBVars

Instances For

def Lean.PrettyPrinter.Delaborator.isSimpleHOFun (motive : Lean.Expr) :

Lean.MetaM Bool

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.isType2Type (motive : Lean.Expr) :

Lean.MetaM Bool

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.isFOLike (motive : Lean.Expr) :

Lean.MetaM Bool

Instances For

def Lean.PrettyPrinter.Delaborator.isIdLike (arg : Lean.Expr) :

Equations

Lean.PrettyPrinter.Delaborator.isIdLike (Lean.Expr.lam binderName binderType (Lean.Expr.bvar deBruijnIndex) binderInfo) = true
Lean.PrettyPrinter.Delaborator.isIdLike arg = false

Instances For

def Lean.PrettyPrinter.Delaborator.isStructureInstance (e : Lean.Expr) :

Lean.MetaM Bool

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.hasMVarAtCurrDepth (e : Lean.Expr) :

Lean.MetaM Bool

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.hasLevelMVarAtCurrDepth (e : Lean.Expr) :

Lean.MetaM Bool

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHBinOp (e : Lean.Expr) :

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.replaceLPsWithVars (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isDefEqAssigning (t s : Lean.Expr) :

Lean.MetaM Bool

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.checkpointDefEq (t s : Lean.Expr) :

Lean.MetaM Bool

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHigherOrder (type : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHigherOrder type = Lean.Meta.forallTelescopeReducing type fun (xs : Array Lean.Expr) (b : Lean.Expr) => pure (decide (xs.size > 0) && b.isSort)

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isFunLike (e : Lean.Expr) :

Lean.MetaM Bool

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isSubstLike (e : Lean.Expr) :

Equations

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isSubstLike e = (e.isAppOfArity `Eq.ndrec 6 || e.isAppOfArity `Eq.rec 6)

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable (n : Lean.Name) :

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum :

Lean.Name → Bool

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.mvarName (mvar : Lean.Expr) :

Lean.MetaM Lean.Name

Equations

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.mvarName mvar = do let __do_lift ← mvar.mvarId!.getDecl pure __do_lift.userName

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.containsBadMax :

Lean.Level → Bool

Instances For

structure Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context :

knowsType : Bool
knowsLevel : Bool
inBottomUp : Bool
parentIsApp : Bool
subExpr : Lean.SubExpr

Instances For

instance Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instInhabitedContext :

Inhabited Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context

Equations

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

structure Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State :

annotations : Lean.PrettyPrinter.Delaborator.OptionsPerPos
postponed : Array (Lean.Expr × Lean.Expr)

Instances For

@[reducible, inline]

abbrev Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM (α : Type) :

Instances For

@[instance 100]

instance Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instMonadReaderOfSubExprAnalyzeM :

MonadReaderOf Lean.SubExpr Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM

@[instance 100]

instance Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instMonadWithReaderOfSubExprAnalyzeM :

MonadWithReaderOf Lean.SubExpr Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.tryUnify (e₁ e₂ : Lean.Expr) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.inspectOutParams (arg mvar : Lean.Expr) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

Instances For

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.inspectOutParams.inspectAux (fType mType : Lean.Expr) (i : Nat) (args mvars : Array Lean.Expr) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isTrivialBottomUp (e : Lean.Expr) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Bool

Equations

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

Instances For

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.canBottomUp (e : Lean.Expr) (mvar? : Option Lean.Expr := none) (fuel : Nat := 10) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Bool

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.withKnowing {α : Type} (knowsType knowsLevel : Bool) (x : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM α) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM α

Instances For

opaque Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeFailureId :

Lean.InternalExceptionId

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.checkKnowsType :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBoolAt (n : Lean.Name) (pos : Lean.SubExpr.Pos) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBool (n : Lean.Name) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

Equations

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

Instances For

structure Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context :

f : Lean.Expr
fType : Lean.Expr
args : Array Lean.Expr
mvars : Array Lean.Expr
bInfos : Array Lean.BinderInfo
forceRegularApp : Bool

Instances For

structure Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State :

bottomUps : Array Bool
higherOrders : Array Bool
funBinders : Array Bool
provideds : Array Bool
namedArgs : Array Lean.Name

Instances For

@[reducible, inline]

abbrev Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM (α : Type) :

Instances For

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze (parentIsApp : Bool := false) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeApp :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeAppStaged (f : Lean.Expr) (args : Array Lean.Expr) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.maybeAddBlockImplicit :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeConst :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

Equations

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

Instances For

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzePi :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeLam :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeLet :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeSort :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

Equations

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeSort = pure ()

Instances For

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeProj :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeFVar :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

Equations

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeFVar = Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.maybeAddBlockImplicit

Instances For

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeMData :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.collectBottomUps :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM PUnit

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.checkOutParams :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM PUnit

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.collectHigherOrders :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM PUnit

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.hBinOpHeuristic :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM PUnit

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.collectTrivialBottomUps :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM PUnit

Equations

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

Instances For

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.applyFunBinderHeuristic :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM PUnit

Instances For

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.applyFunBinderHeuristic.core (args mvars : Array Lean.Expr) (bInfos : Array Lean.BinderInfo) (argIdx : Nat) (mvarType : Lean.Expr) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Bool

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.analyzeFn :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM PUnit

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.annotateNamedArg (n : Lean.Name) :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit

Instances For

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.analyzeArg (i : Nat) :

ReaderT Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context (StateT Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM) PUnit

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.maybeSetExplicit :

Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit

def Lean.PrettyPrinter.Delaborator.topDownAnalyze (e : Lean.Expr) :

Lean.MetaM Lean.PrettyPrinter.Delaborator.OptionsPerPos

Instances For