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 : Options) : Bool

Equations

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

def Lean.getPPAnalyzeCheckInstances (o : Options) : Bool

Equations

• Lean.getPPAnalyzeCheckInstances o = Lean.KVMap.get o Lean.pp.analyze.checkInstances.name Lean.pp.analyze.checkInstances.defValue

def Lean.getPPAnalyzeTypeAscriptions (o : Options) : Bool

Equations

• Lean.getPPAnalyzeTypeAscriptions o = Lean.KVMap.get o Lean.pp.analyze.typeAscriptions.name Lean.pp.analyze.typeAscriptions.defValue

def Lean.getPPAnalyzeTrustSubst (o : Options) : Bool

Equations

• Lean.getPPAnalyzeTrustSubst o = Lean.KVMap.get o Lean.pp.analyze.trustSubst.name Lean.pp.analyze.trustSubst.defValue

def Lean.getPPAnalyzeTrustOfNat (o : Options) : Bool

Equations

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

def Lean.getPPAnalyzeTrustOfScientific (o : Options) : Bool

Equations

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

def Lean.getPPAnalyzeTrustId (o : Options) : Bool

Equations

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

def Lean.getPPAnalyzeTrustSubtypeMk (o : Options) : Bool

Equations

• Lean.getPPAnalyzeTrustSubtypeMk o = Lean.KVMap.get o Lean.pp.analyze.trustSubtypeMk.name Lean.pp.analyze.trustSubtypeMk.defValue

def Lean.getPPAnalyzeTrustKnownFOType2TypeHOFuns (o : Options) : Bool

Equations

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

def Lean.getPPAnalyzeOmitMax (o : Options) : Bool

Equations

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

def Lean.getPPAnalyzeKnowsType (o : Options) : Bool

Equations

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

def Lean.getPPAnalyzeExplicitHoles (o : Options) : Bool

Equations

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

def Lean.getPPAnalysisSkip (o : Options) : Bool

Equations

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

def Lean.getPPAnalysisHole (o : Options) : Bool

Equations

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

def Lean.getPPAnalysisNamedArg (o : Options) : Bool

Equations

• Lean.getPPAnalysisNamedArg o = Lean.KVMap.get o `pp.analysis.namedArg false

def Lean.getPPAnalysisLetVarType (o : Options) : Bool

Equations

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

def Lean.getPPAnalysisNeedsType (o : Options) : Bool

Equations

• Lean.getPPAnalysisNeedsType o = Lean.KVMap.get o `pp.analysis.needsType false

def Lean.getPPAnalysisBlockImplicit (o : Options) : Bool

Equations

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

def Lean.getPPAnalysisNoDot (o : Options) : Bool

Equations

• Lean.getPPAnalysisNoDot o = Lean.KVMap.get o `pp.analysis.noDot false

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

Equations

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

def Lean.PrettyPrinter.Delaborator.isNonConstFun (motive : Expr) : 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

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

Equations

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

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

Equations

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

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

Equations

• Lean.PrettyPrinter.Delaborator.isFOLike motive = pure (motive.getAppFn.isFVar || motive.getAppFn.isConst)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.PrettyPrinter.Delaborator.TopDownAnalyze.checkpointDefEq t s = Lean.Meta.checkpointDefEq (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isDefEqAssigning t s) false

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHigherOrder (type : Expr) : 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)

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum : Name → Bool

Equations

• Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum (p.str str) = Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum p
• Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum (pre.num i) = true
• Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum Lean.Name.anonymous = false

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

Equations

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

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.containsBadMax : Level → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.PrettyPrinter.Delaborator.TopDownAnalyze.containsBadMax u.succ = Lean.PrettyPrinter.Delaborator.TopDownAnalyze.containsBadMax u
• Lean.PrettyPrinter.Delaborator.TopDownAnalyze.containsBadMax x✝ = false

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

• knowsType : Bool
• knowsLevel : Bool
• inBottomUp : Bool
• parentIsApp : Bool
• subExpr : SubExpr

instance Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instInhabitedContext : Inhabited Context

Equations

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

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

• annotations : OptionsPerPos
• postponed : Array (Expr × Expr)

@[reducible, inline]

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

Equations

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

@[instance 100]

instance Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instMonadReaderOfSubExprAnalyzeM : MonadReaderOf SubExpr AnalyzeM

Equations

• Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instMonadReaderOfSubExprAnalyzeM = { read := Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context.subExpr <$> read }

@[instance 100]

instance Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instMonadWithReaderOfSubExprAnalyzeM : MonadWithReaderOf SubExpr AnalyzeM

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

opaque Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeFailureId : InternalExceptionId

def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.checkKnowsType : AnalyzeM Unit

Equations

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

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

Equations

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

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

Equations

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

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

• f : Expr
• fType : Expr
• args : Array Expr
• mvars : Array Expr
• bInfos : Array BinderInfo
• forceRegularApp : Bool

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

• bottomUps : Array Bool
• higherOrders : Array Bool
• funBinders : Array Bool
• provideds : Array Bool
• namedArgs : Array Name

@[reducible, inline]

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

Equations

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

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

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

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

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

Equations

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

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

Equations

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

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

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

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

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

Equations

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

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

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

Equations

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

Equations

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

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.analyzeArg (i : Nat) : ReaderT App.Context (StateT App.State AnalyzeM) PUnit

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

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

Equations

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