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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 (Lean.Expr.hasLooseBVars motive)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

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

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

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

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

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

@[inline, reducible]

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

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

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

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

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

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.inspectOutParams.inspectAux (fType : Lean.Expr) (mType : Lean.Expr) (i : Nat) (args : Array Lean.Expr) (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

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

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

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

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

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

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

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

• f : Lean.Expr
• fType : Lean.Expr
• args : Array Lean.Expr
• mvars : Array Lean.Expr
• bInfos : Array Lean.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 Lake.Name

@[inline, reducible]

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

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze (parentIsApp : optParam 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

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

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

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

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

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

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

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

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

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

partial def Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.applyFunBinderHeuristic.core (args : Array Lean.Expr) (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 : Lake.Name) : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit

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