Skip to content

Commit d796914

Browse files
kim-emclaude
andcommitted
test: add +all -star test case
Verifies that without star fallback, eliminators are not found. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
1 parent d033fc2 commit d796914

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

tests/lean/run/library_search_all.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,3 +69,7 @@ warning: declaration uses 'sorry'
6969
-/
7070
#guard_msgs in
7171
example {α : Sort u} (h : Empty) : α := by exact? +all
72+
73+
/-- error: `exact?` could not close the goal. -/
74+
#guard_msgs in
75+
example {α : Sort u} (h : Empty) : α := by exact? +all -star

0 commit comments

Comments
 (0)