[Merged by Bors] - refactor(tactic/lift): remove attribute/simp-set and swap side goal #16565
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jcommelin
added
awaiting-review
kmill
reviewed
Sep 26, 2022
| @@ -335,7 +335,7 @@ def const_vadd_hom : multiplicative G →* equiv.perm P := | |||
|
|
|||
| variable {P} | |||
|
|
|||
| open function | |||
| open _root_.function | |||
There was a problem hiding this comment.
Is the _root_ necessary, or is it vestigial?
There was a problem hiding this comment.
It is necessary, for reasons I don't understand.
There was a problem hiding this comment.
Oh, it's because there's an equiv.function namespace. I didn't know that _root_ worked in open commands.
I suppose this is fine, but I checked that you can put open function near the beginning of the module. If you don't think that needs to be done, then the PR looks good to me.
There was a problem hiding this comment.
I would prefer to keep it like this.
jcommelin
commented
Sep 26, 2022
|
Thanks! bors r+ |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Sep 27, 2022
…16565) This PR accomplishes two things: * It simplifies the design of the `lift` tactic (while keeping roughly the same user interface, see below). Specifically, it does not need an attribute set to simplify expressions coming from `can_lift` instances. - This will make the tactic easier to port to Lean 4. - It accomplishes this by moving two fields of `can_lift` into `out_param`s. So writing the instances is slightly different from before. * If the `using h` clause is left out, then `lift` produces a subgoal. This subgoal used to come after the main goal. But I think it is natural to make it the first goal. So that you can write ``` lift n to nat with k, { linarith }, ``` instead of ``` lift n to nat using by { linarith } with k, ```
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR accomplishes two things:
lifttactic (while keeping roughly the same user interface, see below). Specifically, it does not need an attribute set to simplify expressions coming fromcan_liftinstances.can_liftintoout_params. So writing the instances is slightly different from before.using hclause is left out, thenliftproduces a subgoal. This subgoal used to come after the main goal. But I think it is natural to make it the first goal. So that you can writeinstead of