Skip to content

Commit e459aaf

Browse files
committed
fix tests
1 parent 78577e2 commit e459aaf

File tree

3 files changed

+9
-9
lines changed

3 files changed

+9
-9
lines changed

tests/lean/run/10213.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f =
1212
theorem bad_csimp : @funnyChoice.{0} = @id.{0} := rfl
1313

1414
/--
15-
error: Tactic `native_decide` failed. Error: failed to compile definition, compiler IR check failed at `_example._nativeDecide_1._closed_0`. Error: depends on declaration 'funnyChoice', which has no executable code; consider marking definition as 'noncomputable'
15+
error: Tactic `native_decide` failed. Error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'funnyChoice', which is 'noncomputable'
1616
-/
1717
#guard_msgs in
1818
example : False := by

tests/lean/run/derivingBEqLinear.lean

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,11 @@ inductive L (α : Type u) : Type u
3434
info: instBEqL.beq_spec.{u_1} {α✝ : Type u_1} [BEq α✝] (x✝ x✝¹ : L α✝) :
3535
(x✝ == x✝¹) =
3636
match decEq x✝.ctorIdx x✝¹.ctorIdx with
37-
| isTrue h =>
37+
| { decide := true, reflects_decide := h } =>
3838
match x✝, x✝¹, h with
3939
| L.nil, L.nil, ⋯ => true
4040
| L.cons a a_1, L.cons a' a'_1, ⋯ => a == a' && a_1 == a'_1
41-
| isFalse h => false
41+
| { decide := false, reflects_decide := h } => false
4242
-/
4343
#guard_msgs in #check instBEqL.beq_spec
4444

@@ -65,11 +65,11 @@ info: @[expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α]
6565
info: theorem InNamespace.instBEqL'.beq_spec.{u_1} : ∀ {α : Type u_1} [inst : BEq α] (x x_1 : InNamespace.L' α),
6666
(x == x_1) =
6767
match decEq x.ctorIdx x_1.ctorIdx with
68-
| isTrue h =>
68+
| { decide := true, reflects_decide := h } =>
6969
match x, x_1, h with
7070
| InNamespace.L'.nil, InNamespace.L'.nil, ⋯ => true
7171
| InNamespace.L'.cons a a_1, InNamespace.L'.cons a' a'_1, ⋯ => a == a' && a_1 == a'_1
72-
| isFalse h => false
72+
| { decide := false, reflects_decide := h } => false
7373
-/
7474
#guard_msgs in #print sig InNamespace.instBEqL'.beq_spec
7575

@@ -82,11 +82,11 @@ inductive Vec (α : Type u) : Nat → Type u
8282
info: instBEqVec.beq_spec.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] (x✝ x✝¹ : Vec α✝ a✝) :
8383
(x✝ == x✝¹) =
8484
match decEq x✝.ctorIdx x✝¹.ctorIdx with
85-
| isTrue h =>
85+
| { decide := true, reflects_decide := h } =>
8686
match a✝, x✝, x✝¹ with
8787
| 0, Vec.nil, Vec.nil, ⋯ => true
8888
| x + 1, Vec.cons a a_1, Vec.cons a' a'_1, ⋯ => a == a' && a_1 == a'_1
89-
| isFalse h => false
89+
| { decide := false, reflects_decide := h } => false
9090
-/
9191
#guard_msgs in
9292
#check instBEqVec.beq_spec

tests/lean/run/reduceBEqSimproc.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,11 +31,11 @@ deriving BEq
3131
info: Linear.instBEqL.beq.eq_1.{u_1} {α✝ : Type u_1} [BEq α✝] (x✝ x✝¹ : L α✝) :
3232
instBEqL.beq x✝ x✝¹ =
3333
match decEq x✝.ctorIdx x✝¹.ctorIdx with
34-
| isTrue h =>
34+
| { decide := true, reflects_decide := h } =>
3535
match x✝, x✝¹, h with
3636
| L.nil, L.nil, ⋯ => true
3737
| L.cons a a_1, L.cons a' a'_1, ⋯ => a == a' && instBEqL.beq a_1 a'_1
38-
| isFalse h => false
38+
| { decide := false, reflects_decide := h } => false
3939
-/
4040
#guard_msgs in
4141
#check instBEqL.beq.eq_1

0 commit comments

Comments
 (0)