Skip to content

Commit 251da9f

Browse files
committed
Fix error
1 parent cce3435 commit 251da9f

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Elab/App.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1424,7 +1424,7 @@ where
14241424
type{inlineExprTrailing eType}"
14251425

14261426
-- Possible alternatives provided with `@[suggest_for]` annotations
1427-
let suggestions := (← Lean.getSuggestions fullName).filter (·.getPrefix = fullName.getPrefix)
1427+
let suggestions := (← Lean.getSuggestions fullName).filter (·.getPrefix = fullName.getPrefix) |>.toArray
14281428
let suggestForHint ←
14291429
if h : suggestions.size = 0 then
14301430
pure .nil

0 commit comments

Comments
 (0)