Equations
- Lean.getPPAnalyze o = Lean.KVMap.get o Lean.pp.analyze.name Lean.pp.analyze.defValue
Equations
Equations
Equations
Equations
Equations
Equations
- Lean.getPPAnalyzeTrustId o = Lean.KVMap.get o Lean.pp.analyze.trustId.name Lean.pp.analyze.trustId.defValue
Equations
- Lean.getPPAnalyzeTrustCoe o = Lean.KVMap.get o Lean.pp.analyze.trustCoe.name Lean.pp.analyze.trustCoe.defValue
Equations
Equations
- Lean.getPPAnalyzeOmitMax o = Lean.KVMap.get o Lean.pp.analyze.omitMax.name Lean.pp.analyze.omitMax.defValue
Equations
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.PrettyPrinter.Delaborator.returnsPi motive = Lean.Meta.lambdaTelescope motive fun xs b => pure (Lean.Expr.isForall b)
Equations
Equations
- Lean.PrettyPrinter.Delaborator.isSimpleHOFun motive = do let a ← Lean.PrettyPrinter.Delaborator.returnsPi motive let a_1 ← Lean.PrettyPrinter.Delaborator.isNonConstFun motive pure (!a && !a_1)
Equations
- Lean.PrettyPrinter.Delaborator.isType2Type motive = do let a ← Lean.Meta.inferType motive match a with | Lean.Expr.forallE x (Lean.Expr.sort x_1 x_2) (Lean.Expr.sort x_3 x_4) x_5 => pure true | x => pure false
Equations
- Lean.PrettyPrinter.Delaborator.isFOLike motive = let f := Lean.Expr.getAppFn motive; pure (Lean.Expr.isFVar f || Lean.Expr.isConst f)
Equations
- Lean.PrettyPrinter.Delaborator.isIdLike arg = match arg with | Lean.Expr.lam x x_1 (Lean.Expr.bvar x_2 x_3) x_4 => true | x => false
Equations
- Lean.PrettyPrinter.Delaborator.isCoe e = (Lean.Expr.isAppOfArity e `CoeT.coe 4 || Lean.Expr.isAppOf e `CoeFun.coe && decide (Lean.Expr.getAppNumArgs e ≥ 4) || Lean.Expr.isAppOfArity e `CoeSort.coe 4)
Equations
- Lean.PrettyPrinter.Delaborator.isStructureInstance e = do let a ← Lean.getEnv match Lean.Expr.isConstructorApp? a e with | some s => do let a ← Lean.getEnv pure (Lean.isStructure a s.induct) | none => pure false
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.hasMVarAtCurrDepth e = do let mctx ← Lean.getMCtx pure (Option.isSome (Lean.Expr.findMVar? e fun mvarId => match Lean.MetavarContext.findDecl? mctx mvarId with | some mdecl => mdecl.depth == mctx.depth | x => false))
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.hasLevelMVarAtCurrDepth e = do let mctx ← Lean.getMCtx pure (Option.isSome (Lean.Expr.findLevelMVar? e fun mvarId => Lean.MetavarContext.findLevelDepth? mctx mvarId == some mctx.depth))
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHBinOp e = Id.run (let _do_jp := fun y => let f := Lean.Expr.getAppFn e; let _do_jp := fun y => let ops := #[`HOr.hOr, `HXor.hXor, `HAnd.hAnd, `HAppend.hAppend, `HOrElse.hOrElse, `HAndThen.hAndThen, `HAdd.hAdd, `HSub.hSub, `HMul.hMul, `HDiv.hDiv, `HMod.hMod, `HShiftLeft.hShiftLeft, `HShiftRight]; Array.any ops (fun op => op == Lean.Expr.constName! f) 0 (Array.size ops); if (!Lean.Expr.isConst f) = true then pure false else do let y ← pure PUnit.unit _do_jp y; if (Lean.Expr.getAppNumArgs e != 6) = true then pure false else do let y ← pure PUnit.unit _do_jp y)
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.replaceLPsWithVars e = let _do_jp := fun y => let lps := (Lean.collectLevelParams { visitedLevel := ∅, visitedExpr := ∅, params := #[] } e).params; let replaceMap := ∅; do let r ← forIn lps replaceMap fun lp r => let replaceMap := r; do let a ← Lean.Meta.mkFreshLevelMVar let replaceMap : Std.HashMap Lean.Name Lean.Level := Std.HashMap.insert replaceMap lp a pure PUnit.unit pure (ForInStep.yield replaceMap) let x : Std.HashMap Lean.Name Lean.Level := r let replaceMap : Std.HashMap Lean.Name Lean.Level := x pure (Lean.Expr.replaceLevel (fun x => match x with | Lean.Level.param n x => some (Std.HashMap.find! replaceMap n) | l => if (!Lean.Level.hasParam l) = true then some l else none) e); if (!Lean.Expr.hasLevelParam e) = true then pure e else do let y ← pure PUnit.unit _do_jp y
def
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isDefEqAssigning
(t : Lean.Expr)
(s : Lean.Expr)
:
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isDefEqAssigning t s = withReader (fun ctx => { config := let src := ctx.config; { foApprox := src.foApprox, ctxApprox := src.ctxApprox, quasiPatternApprox := src.quasiPatternApprox, constApprox := src.constApprox, isDefEqStuckEx := src.isDefEqStuckEx, transparency := src.transparency, zetaNonDep := src.zetaNonDep, trackZeta := src.trackZeta, unificationHints := src.unificationHints, proofIrrelevance := src.proofIrrelevance, assignSyntheticOpaque := true, ignoreLevelMVarDepth := src.ignoreLevelMVarDepth, offsetCnstrs := src.offsetCnstrs, etaStruct := src.etaStruct }, lctx := ctx.lctx, localInstances := ctx.localInstances, defEqCtx? := ctx.defEqCtx?, synthPendingDepth := ctx.synthPendingDepth, canUnfold? := ctx.canUnfold? }) (Lean.Meta.isDefEq t s)
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHigherOrder type = Lean.Meta.forallTelescopeReducing type fun xs b => pure (decide (Array.size xs > 0) && Lean.Expr.isSort b)
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isFunLike e = do let a ← Lean.Meta.inferType e Lean.Meta.forallTelescopeReducing a fun xs b => pure (decide (Array.size xs > 0))
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isSubstLike e = (Lean.Expr.isAppOfArity e `Eq.ndrec 6 || Lean.Expr.isAppOfArity e `Eq.rec 6)
Equations
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum (Lean.Name.str p x_1 x_2) = Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum p
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum (Lean.Name.num x_1 x_2 x_3) = true
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum Lean.Name.anonymous = false
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.mvarName mvar = do let a ← Lean.Meta.getMVarDecl (Lean.Expr.mvarId! mvar) pure a.userName
- knowsType : Bool
- knowsLevel : Bool
- inBottomUp : Bool
- parentIsApp : Bool
- subExpr : Lean.PrettyPrinter.Delaborator.SubExpr
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instInhabitedContext = { default := { knowsType := default, knowsLevel := default, inBottomUp := default, parentIsApp := default, subExpr := default } }
- annotations : Std.RBMap Lean.PrettyPrinter.Delaborator.Pos Lean.Options compare
- postponed : Array (Lean.Expr × Lean.Expr)
@[inline]
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instMonadWithReaderOfSubExprAnalyzeM = { withReader := fun {α} f x ctx => x { knowsType := ctx.knowsType, knowsLevel := ctx.knowsLevel, inBottomUp := ctx.inBottomUp, parentIsApp := ctx.parentIsApp, subExpr := f ctx.subExpr } }
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.tryUnify e₁ e₂ = tryCatch (do let r ← liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isDefEqAssigning e₁ e₂) let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit := fun y => pure () if (!r) = true then do let y ← modify fun s => { annotations := s.annotations, postponed := Array.push s.postponed (e₁, e₂) } _do_jp y else do let y ← pure PUnit.unit _do_jp y) fun ex => modify fun s => { annotations := s.annotations, postponed := Array.push s.postponed (e₁, e₂) }
def
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.inspectOutParams
(arg : Lean.Expr)
(mvar : Lean.Expr)
:
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.inspectOutParams arg mvar = (fun inspectAux => do let argType ← liftM (Lean.Meta.inferType arg) let mvarType ← liftM (Lean.Meta.inferType mvar) let fType ← liftM (Lean.Meta.inferType (Lean.Expr.getAppFn argType)) let mType ← liftM (Lean.Meta.inferType (Lean.Expr.getAppFn mvarType)) inspectAux fType mType 0 (Lean.Expr.getAppArgs argType) (Lean.Expr.getAppArgs mvarType)) Lean.PrettyPrinter.Delaborator.TopDownAnalyze.inspectOutParams.inspectAux
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isTrivialBottomUp e = do let opts ← Lean.getOptions pure (Lean.Expr.isFVar e || Lean.Expr.isConst e || Lean.Expr.isMVar e || Lean.Expr.isNatLit e || Lean.Expr.isStringLit e || Lean.Expr.isSort e || Lean.getPPAnalyzeTrustOfNat opts && Lean.Expr.isAppOfArity e `OfNat.ofNat 3 || Lean.getPPAnalyzeTrustOfScientific opts && Lean.Expr.isAppOfArity e `OfScientific.ofScientific 5)
def
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.withKnowing
{α : Type}
(knowsType : Bool)
(knowsLevel : Bool)
(x : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM α)
:
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.withKnowing knowsType knowsLevel x = withReader (fun ctx => { knowsType := knowsType, knowsLevel := knowsLevel, inBottomUp := ctx.inBottomUp, parentIsApp := ctx.parentIsApp, subExpr := ctx.subExpr }) x
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.checkKnowsType = do let a ← read if (!a.knowsType) = true then throw (Lean.Exception.internal Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeFailureId) else pure PUnit.unit
def
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBoolAt
(n : Lean.Name)
(pos : Lean.PrettyPrinter.Delaborator.Pos)
:
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBoolAt n pos = do let a ← get let opts : Lean.KVMap := Lean.KVMap.setBool (Std.RBMap.findD a.annotations pos { entries := [] }) n true let cls : Lean.Name := `pp.analyze.annotate let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit := fun y => modify fun s => { annotations := Std.RBMap.insert s.annotations pos opts, postponed := s.postponed } if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData pos ++ Lean.toMessageData " " ++ Lean.toMessageData n ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBool n = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getPos Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBoolAt n a
@[inline]
partial def
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze
(parentIsApp : optParam Bool false)
:
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.maybeAddBlockImplicit = do let a ← read if (!a.parentIsApp) = true then do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let type ← liftM (Lean.Meta.inferType a) if (Lean.Expr.isForall type && Lean.Expr.bindingInfo! type == Lean.BinderInfo.implicit) = true then Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBool `pp.analysis.blockImplicit else pure PUnit.unit else pure PUnit.unit
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeConst = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.const n ls x => do let a ← read let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit := fun y => Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.maybeAddBlockImplicit if (!a.knowsLevel && !List.isEmpty ls) = true then do let a ← Lean.getOptions if (Lean.getPPAnalyzeOmitMax a && List.any ls Lean.PrettyPrinter.Delaborator.TopDownAnalyze.containsBadMax) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBool `pp.universes _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.TopDownAnalyze" "Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeConst" 443 41 "unreachable code has been reached"
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.collectBottomUps = do let discr ← read let x : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context := discr match x with | { f := x, fType := x_1, args := args, mvars := mvars, bInfos := bInfos, forceRegularApp := x_2 } => do let r ← let col := [fun x => none, fun i => some (Array.getOp mvars i)]; forIn col PUnit.unit fun target r => do let r ← let col := { start := 0, stop := Array.size args, step := 1 }; forIn col PUnit.unit fun i r => if (Array.getOp bInfos i == Lean.BinderInfo.default) = true then do let a ← liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.typeUnknown (Array.getOp mvars i)) <&&> liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.canBottomUp (Array.getOp args i) (target i) 10) if a = true then do liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.tryUnify (Array.getOp args i) (Array.getOp mvars i)) modify fun s => { bottomUps := Array.set! s.bottomUps i true, higherOrders := s.higherOrders, funBinders := s.funBinders, provideds := s.provideds, namedArgs := s.namedArgs } pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.checkOutParams = do let discr ← read let x : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context := discr match x with | { f := x, fType := x_1, args := args, mvars := mvars, bInfos := bInfos, forceRegularApp := x_2 } => do let r ← let col := { start := 0, stop := Array.size args, step := 1 }; forIn col PUnit.unit fun i r => if (Array.getOp bInfos i == Lean.BinderInfo.instImplicit) = true then do liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.inspectOutParams (Array.getOp args i) (Array.getOp mvars i)) pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.collectHigherOrders = do let discr ← read let x : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context := discr match x with | { f := x, fType := x_1, args := args, mvars := mvars, bInfos := bInfos, forceRegularApp := x_2 } => do let r ← let col := { start := 0, stop := Array.size args, step := 1 }; forIn col PUnit.unit fun i r => let _do_jp := fun y => do let a ← liftM (Lean.Meta.inferType (Array.getOp args i)) let a ← liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHigherOrder a) let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM (ForInStep PUnit) := fun y => do let a ← Lean.getOptions let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM (ForInStep PUnit) := fun y => do let a ← Lean.getOptions let a_1 ← liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.valUnknown (Array.getOp mvars i)) let a_2 ← liftM (Lean.PrettyPrinter.Delaborator.isType2Type (Array.getOp args i)) let a_3 ← liftM (Lean.PrettyPrinter.Delaborator.isFOLike (Array.getOp args i)) let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM (ForInStep PUnit) := fun y => do liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.tryUnify (Array.getOp args i) (Array.getOp mvars i)) modify fun s => { bottomUps := s.bottomUps, higherOrders := Array.set! s.higherOrders i true, funBinders := s.funBinders, provideds := s.provideds, namedArgs := s.namedArgs } pure (ForInStep.yield PUnit.unit) if (Lean.getPPAnalyzeTrustKnownFOType2TypeHOFuns a && !a_1 && a_2 && a_3) = true then pure (ForInStep.yield PUnit.unit) else do let y ← pure PUnit.unit _do_jp y if (Lean.getPPAnalyzeTrustId a && Lean.PrettyPrinter.Delaborator.isIdLike (Array.getOp args i)) = true then pure (ForInStep.yield PUnit.unit) else do let y ← pure PUnit.unit _do_jp y if (!a) = true then pure (ForInStep.yield PUnit.unit) else do let y ← pure PUnit.unit _do_jp y; if (!(Array.getOp bInfos i == Lean.BinderInfo.implicit || Array.getOp bInfos i == Lean.BinderInfo.strictImplicit)) = true then pure (ForInStep.yield PUnit.unit) else do let y ← pure PUnit.unit _do_jp y let x : PUnit := r pure PUnit.unit
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.hBinOpHeuristic = do let discr ← read let x : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context := discr match x with | { f := x, fType := x_1, args := args, mvars := mvars, bInfos := bInfos, forceRegularApp := x_2 } => do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let a ← pure (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHBinOp a) <&&> (liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.valUnknown (Array.getOp mvars 0)) <||> liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.valUnknown (Array.getOp mvars 1))) if a = true then liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.tryUnify (Array.getOp mvars 0) (Array.getOp mvars 1)) else pure PUnit.unit
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.collectTrivialBottomUps = do let discr ← read let x : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context := discr match x with | { f := x, fType := x_1, args := args, mvars := mvars, bInfos := bInfos, forceRegularApp := x_2 } => do let r ← let col := { start := 0, stop := Array.size args, step := 1 }; forIn col PUnit.unit fun i r => if (Array.getOp bInfos i == Lean.BinderInfo.default) = true then do let a ← liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.valUnknown (Array.getOp mvars i)) <&&> liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isTrivialBottomUp (Array.getOp args i)) if a = true then do liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.tryUnify (Array.getOp args i) (Array.getOp mvars i)) modify fun s => { bottomUps := Array.set! s.bottomUps i true, higherOrders := s.higherOrders, funBinders := s.funBinders, provideds := s.provideds, namedArgs := s.namedArgs } pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.applyFunBinderHeuristic = do let discr ← read let x : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context := discr match x with | { f := f, fType := x, args := args, mvars := mvars, bInfos := bInfos, forceRegularApp := x_1 } => (fun core => do let r ← let col := { start := 0, stop := Array.size args, step := 1 }; forIn col PUnit.unit fun i r => do let a ← pure (Array.getOp bInfos i == Lean.BinderInfo.default) if a = true then do let a ← liftM (Lean.Meta.inferType (Array.getOp mvars i)) let b ← Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg i (core i a) if b = true then do modify fun s => { bottomUps := s.bottomUps, higherOrders := s.higherOrders, funBinders := Array.set! s.funBinders i true, provideds := s.provideds, namedArgs := s.namedArgs } pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit) (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.applyFunBinderHeuristic.core args mvars bInfos)
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)
:
def
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.annotateNamedArg
(n : Lean.Name)
:
Equations
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.annotateNamedArg n = do liftM (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBool `pp.analysis.namedArg) modify fun s => { bottomUps := s.bottomUps, higherOrders := s.higherOrders, funBinders := s.funBinders, provideds := s.provideds, namedArgs := Array.push s.namedArgs n }
Equations
- Lean.PrettyPrinter.Delaborator.topDownAnalyze e = do let s₀ ← get Lean.traceCtx `pp.analyze (withReader (fun ctx => { config := Lean.Elab.Term.setElabConfig ctx.config, lctx := ctx.lctx, localInstances := ctx.localInstances, defEqCtx? := ctx.defEqCtx?, synthPendingDepth := ctx.synthPendingDepth, canUnfold? := ctx.canUnfold? }) (let ϕ := do Lean.Meta.withNewMCtxDepth (Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze false) let a ← get pure a.annotations; tryFinally (tryCatch (do let a ← Lean.getOptions let knowsType : Bool := Lean.getPPAnalyzeKnowsType a StateRefT'.run' (ϕ { knowsType := knowsType, knowsLevel := knowsType, inBottomUp := false, parentIsApp := false, subExpr := Lean.PrettyPrinter.Delaborator.SubExpr.mkRoot e }) { annotations := ∅, postponed := #[] }) fun ex => let cls := `pp.analyze.error; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.PrettyPrinter.Delaborator.OptionsPerPos := fun y => pure ∅ if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "failed") _do_jp y else do let y ← pure PUnit.unit _do_jp y) (set s₀)))