From 548bf4d9f4735a19c22604b7ff173f1d473ef47f Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Wed, 28 Jul 2021 17:37:37 -0700 Subject: [PATCH] chore: rm stale todo --- src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 37877eb6ed..c6475b9b1f 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -276,7 +276,6 @@ where tryUnify (← inferType (mkAppN f args)) resultType -- Collect explicit arguments that can be elaborated without expected type - -- TODO: try before *and* after HO? let mut bottomUps := mkArray args.size false for i in [:args.size] do if bInfos[i] == BinderInfo.default then @@ -346,8 +345,6 @@ where annotateBool `pp.analysis.needsExplicit true analyzeConst : AnalyzeM Unit := do - -- TODO: currently, the analyzer never uses @ for applications, - -- even though named arguments do not work for inaccessible names let Expr.const n ls .. ← getExpr | unreachable! annotateBool `pp.universes (!(← read).knowsLevel && !ls.isEmpty) maybeAddExplicit