Skip to content

Commit 7c3ca70

Browse files
committed
chore: fix test
1 parent 964db5b commit 7c3ca70

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

tests/lean/run/grind_trace.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,9 +34,9 @@ example : 0 < (x :: t).length := by
3434

3535
attribute [grind ext] List.ext_getElem?
3636
/--
37-
info: Try this: grind only [= List.length_replicate, = List.getElem?_eq_none, = List.getElem?_eq_getElem,
38-
= List.getElem?_eq_some_iff, = Option.map_some, = Option.map_none, = List.getElem?_replicate,
39-
= List.getElem_replicate, = List.getElem?_map]
37+
info: Try this: grind only [= List.length_replicate, = List.getElem?_eq_none, = List.getElem?_eq_getElem, =
38+
List.getElem?_eq_some_iff, = Option.map_some, = Option.map_none, = List.getElem?_replicate, = List.getElem_replicate,
39+
= List.getElem?_map]
4040
-/
4141
#guard_msgs (info) in
4242
theorem map_replicate' : (List.replicate n a).map f = List.replicate n (f a) := by

0 commit comments

Comments
 (0)