diff --git a/tests/lean/crash.lean b/tests/lean/crash.lean index b65542a4d5..e8b4601729 100644 --- a/tests/lean/crash.lean +++ b/tests/lean/crash.lean @@ -3,7 +3,7 @@ import logic section hypothesis P : Prop. -theorem crash +definition crash := assume H : P, have H' : ¬ P, from H,