From 941a68165aa53ddeb3faef5e2c5162e5b1491c88 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 21 Jan 2021 17:23:17 +0100
Subject: [PATCH] fix: hover/definition for applications with only implicit
 arguments

---
 src/Lean/Elab/App.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 5921f77649..b39dee70e8 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -770,8 +770,7 @@ private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level)
   -- Set `errToSorry` to `false` if `funLVals` > 1. See comment above about the interaction between `errToSorry` and `observing`.
   withReader (fun ctx => { ctx with errToSorry := funLVals.length == 1 && ctx.errToSorry }) do
     funLVals.foldlM (init := acc) fun acc (f, fIdent, fields) => do
-      unless lvals.isEmpty && args.isEmpty && namedArgs.isEmpty && fields.isEmpty do
-        addTermInfo fIdent f
+      addTermInfo fIdent f
       let lvals' := fields.map fun field => LVal.fieldName field field.getId.toString
       let s ← observing do
         let e ← elabAppLVals f (lvals' ++ lvals) namedArgs args expectedType? explicit ellipsis