Skip to content

Commit 7b5953b

Browse files
committed
fix that one test
1 parent 8b39e0d commit 7b5953b

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

tests/lean/run/4644.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ because its `Decidable` instance
3333
did not reduce to `isTrue` or `isFalse`.
3434
3535
After unfolding the instances `instDecidableEqBool`, `Bool.decEq`, and `Nat.decLe`, reduction got stuck at
36-
sorted_from_var #[0, 3, 3, 5, 8, 10, 10, 10] 0
36+
sorted_to_var #[0, 3, 3, 5, 8, 10, 10, 10] (#[0, 3, 3, 5, 8, 10, 10, 10].size - 2) ⋯
3737
-/
3838
#guard_msgs in
3939
example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by

0 commit comments

Comments
 (0)