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.
Equations
Equations
- Lean.getPPAnalysisSkip o = Lean.KVMap.get o `pp.analysis.skip false
Equations
- Lean.getPPAnalysisHole o = Lean.KVMap.get o `pp.analysis.hole false
Equations
- Lean.getPPAnalysisNamedArg o = Lean.KVMap.get o `pp.analysis.namedArg false
Equations
- Lean.getPPAnalysisLetVarType o = Lean.KVMap.get o `pp.analysis.letVarType false
Equations
- Lean.getPPAnalysisNeedsType o = Lean.KVMap.get o `pp.analysis.needsType false
Equations
- Lean.getPPAnalysisBlockImplicit o = Lean.KVMap.get o `pp.analysis.blockImplicit false
Equations
- Lean.getPPAnalysisNoDot o = Lean.KVMap.get o `pp.analysis.noDot false
Equations
- Lean.PrettyPrinter.Delaborator.returnsPi motive = Lean.Meta.lambdaTelescope motive fun (x : Array Lean.Expr) (b : Lean.Expr) => pure b.isForall
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
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.PrettyPrinter.Delaborator.isIdLike (Lean.Expr.lam binderName binderType (Lean.Expr.bvar deBruijnIndex) binderInfo) = true
- Lean.PrettyPrinter.Delaborator.isIdLike arg = false
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isSubstLike e = (e.isAppOfArity `Eq.ndrec 6 || e.isAppOfArity `Eq.rec 6)
Equations
- One or more equations did not get rendered due to their size.
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
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
Equations
- One or more equations did not get rendered due to their size.
- annotations : OptionsPerPos
@[reducible, inline]
Equations
- One or more equations did not get rendered due to their size.
@[instance 100]
@[instance 100]
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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)
:
def
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.annotateNamedArg
(n : Name)
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.