Skip to content

Commit bd4c98a

Browse files
committed
fix test
1 parent df05564 commit bd4c98a

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

tests/lean/zetaDeltaFVarIdsLeakage.lean

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,10 @@ example : True := by
66
have : 1 = 1 := by simp?
77
trivial
88

9+
axiom test_sorry {α : Sort _} : α
10+
911
example : False := by
1012
let a := 1
1113
let b := 1
12-
have : a = 1 → False := sorry
14+
have : a = 1 → False := test_sorry
1315
simp (disch := simp [b]) [this, a]

0 commit comments

Comments
 (0)