Skip to content

Commit 8795c08

Browse files
committed
fix tests, rename
1 parent bc68352 commit 8795c08

File tree

5 files changed

+2
-2
lines changed

5 files changed

+2
-2
lines changed
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
import Lean.LibrarySuggestions.Basic
22

33
/--
4-
error: No premise selector registered. (Note that Lean does not provide a default premise selector, these must be provided by a downstream library, and configured using `set_premise_selector`.)
4+
error: No library suggestions engine registered. (Note that Lean does not provide a default library suggestions engine, these must be provided by a downstream library, and configured using `set_library_suggestions`.)
55
-/
66
#guard_msgs in
77
example : True := by
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ error: Failed to elaborate Nat as a `MVarId → Config → MetaM (Array Suggesti
1515
set_library_suggestions Nat
1616

1717
/--
18-
error: No premise selector registered. (Note that Lean does not provide a default premise selector, these must be provided by a downstream library, and configured using `set_library_suggestions`.)
18+
error: No library suggestions engine registered. (Note that Lean does not provide a default library suggestions engine, these must be provided by a downstream library, and configured using `set_library_suggestions`.)
1919
-/
2020
#guard_msgs in
2121
example : True := by
File renamed without changes.
File renamed without changes.
File renamed without changes.

0 commit comments

Comments
 (0)