-
Notifications
You must be signed in to change notification settings - Fork 259
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
apply?/exact?/have?/rw? issues #3426
Comments
Should
work? The flipped version successfully finds |
|
@semorrison I hope you don't mind that I hijacked your first comment here to keep track of some Zulip threads where I reported issues. |
import Mathlib
example {n : ℕ} : n = 0 ∨ 0 < n := by exact? -- Fails to find `eq_zero_or_pos` including reply from @dwrensha pointing out that this is a consequence of the mathlib4/Mathlib/Lean/Expr/Basic.lean Line 97 in a1451be
|
import Mathlib.Tactic
example (h : ¬P ∨ Q) (h' : P) : Q := by exact? -- fails
example (h : ¬P ∨ Q) (h' : P) : Q := imp_iff_not_or.mpr h h' |
@grhkm21 I believe this is an intentional limitation: some lemmas apply to every goal, and for performance reasons they are not tried by |
But it might well be possible to re-enable trying these universal lemmas, as in the current model they would be tried last, and we have an automatic mechanism to stop before reaching a timeout. Someone should try! |
import Mathlib
example (x y c : ℝ) (h: 0 < c) : x < y → c * x < c * y := by exact? suggests the malformed term
|
Please list bugs in these tactics here.
apply?
suggestionrw?
errors and panicsapply?
cache corrupts on updateThe text was updated successfully, but these errors were encountered: