We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b85953a commit b3bd6d2Copy full SHA for b3bd6d2
tests/lean/run/grind_indexmap.lean
@@ -6,7 +6,7 @@ import Std.Data.HashMap
6
7
set_option grind.warning false
8
9
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| grind)
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
10
11
open Std
12
0 commit comments