Skip to content

Commit 3341915

Browse files
committed
fix iterators test
1 parent 955dcc6 commit 3341915

File tree

1 file changed

+6
-6
lines changed

1 file changed

+6
-6
lines changed

tests/lean/run/iterators.lean

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -362,28 +362,28 @@ example := positives.toListRev
362362
example := positives.toArray
363363

364364
/--
365-
error: failed to synthesize
365+
error: failed to synthesize instance of type class
366366
Std.Iterators.Finite (Std.Iterators.RepeatIterator Nat fun x => x + 1) Id
367367
368-
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
368+
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
369369
-/
370370
#guard_msgs in
371371
example := positives.ensureTermination.toList
372372

373373
/--
374-
error: failed to synthesize
374+
error: failed to synthesize instance of type class
375375
Std.Iterators.Finite (Std.Iterators.RepeatIterator Nat fun x => x + 1) Id
376376
377-
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
377+
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
378378
-/
379379
#guard_msgs in
380380
example := positives.ensureTermination.toListRev
381381

382382
/--
383-
error: failed to synthesize
383+
error: failed to synthesize instance of type class
384384
Std.Iterators.Finite (Std.Iterators.RepeatIterator Nat fun x => x + 1) Id
385385
386-
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
386+
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
387387
-/
388388
#guard_msgs in
389389
example := positives.ensureTermination.toArray

0 commit comments

Comments
 (0)