Skip to content

Commit 43907aa

Browse files
committed
chore: fix tests
1 parent 677e803 commit 43907aa

File tree

1 file changed

+6
-6
lines changed

1 file changed

+6
-6
lines changed

tests/lean/run/grind_const_pattern.lean

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ h : ¬a = 10
1919
[eqc] False propositions
2020
[prop] a = 10
2121
[cutsat] Assignment satisfying linear constraints
22-
[assign] a := 0
22+
[assign] a := 1
2323
-/
2424
#guard_msgs (error) in
2525
example : a = 5 + 5 := by
@@ -50,8 +50,8 @@ h : ¬f a = 11
5050
[eqc] False propositions
5151
[prop] f a = 11
5252
[cutsat] Assignment satisfying linear constraints
53-
[assign] a := 1
54-
[assign] f a := 0
53+
[assign] a := 2
54+
[assign] f a := 1
5555
-/
5656
#guard_msgs (error) in
5757
example : f a = 10 + 1 := by
@@ -76,9 +76,9 @@ h : ¬f x = 11
7676
[ematch] E-matching patterns
7777
[thm] fa: [f `[a]]
7878
[cutsat] Assignment satisfying linear constraints
79-
[assign] x := 2
80-
[assign] a := 1
81-
[assign] f x := 0
79+
[assign] x := 3
80+
[assign] a := 2
81+
[assign] f x := 1
8282
-/
8383
#guard_msgs (error) in
8484
example : f x = 10 + 1 := by

0 commit comments

Comments
 (0)