We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
obtain
import tactic.rcases example : true := begin obtain h : true, { trivial }, success_if_fail { exact h }, assumption, end
Note that this behaviour does not happen if the term is created using :=:
:=
example : true := begin obtain h : true := trivial, exact h end
Found whilst making #15735.
The text was updated successfully, but these errors were encountered:
The bug goes a bit higher; to rcases; rcases h with t will just let the hypothesis remain named h instead of renaming it to t.
rcases
rcases h with t
h
t
Sorry, something went wrong.
feat(tactic/rcases): support rcases x with y renames
rcases x with y
83dfad8
fixes #15741
073a3e9
fix(tactic/rcases): support rcases x with y renames (#15773)
63971d1
edbb6e4
Successfully merging a pull request may close this issue.
Note that this behaviour does not happen if the term is created using
:=
:Found whilst making #15735.
The text was updated successfully, but these errors were encountered: