chore: rwa tactic macro
#3299
Merged
chore: rwa tactic macro
#3299
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
This commit also allows the `rfl` tactic to be used as shorthand for `Iff.rfl` and `HEq.rfl`
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
nomeata
reviewed
Feb 10, 2024
| @@ -323,9 +323,14 @@ syntax (name := eqRefl) "eq_refl" : tactic | |||
| `rfl` tries to close the current goal using reflexivity. | |||
| This is supposed to be an extensible tactic and users can add their own support | |||
| for new reflexive relations. | |||
|
|
|||
| Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different | |||
| reflexivity theorems (e.g., `Iff.rfl`). | |||
There was a problem hiding this comment.
“We later add” doesn't quite work well for a user facing docstring, does it?
nomeata
reviewed
Feb 10, 2024
| /-- `rwa` calls `rw`, then closes any remaining goals using `assumption`. -/ | ||
| macro "rwa " rws:rwRuleSeq loc:(location)? : tactic => | ||
| `(tactic| (rw $rws:rwRuleSeq $[$loc:location]?; assumption)) | ||
|
|
There was a problem hiding this comment.
The docstring says “any goals” but the code looks like it will close exactly one goal. Should the docstring say “the remaining goal”?
nomeata
reviewed
Feb 10, 2024
| has type | ||
| ?m ↔ ?m : Prop | ||
| but is expected to have type | ||
| b ≤ 2 : Prop |
There was a problem hiding this comment.
This seems to be a slight regression of error reporting, but for something so elementary as rfl not irrelevant.
If macro rules are used, which tactic decides about the error message? Last or first? Can we somehow register a fail "trivial equality (or equivalence) expected" or simply fail "rfl failed" or something like this as the last tactic to try with rfl?
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.
No description provided.