doc: revise show tactic documentation to more accurately describe its behavior
#7389
Conversation
euprunin
changed the title
show tactic documentation to more accurately describe its behaviorshow tactic documentation to more accurately describe its behavior
euprunin
force-pushed
the
fix-show-documentation
branch
from
a71e805 to
7a31bdc
Compare
| @@ -791,10 +791,11 @@ The `let` tactic is for adding definitions to the local context of the main goal | |||
| -/ | |||
| macro "let " d:letDecl : tactic => `(tactic| refine_lift let $d:letDecl; ?_) | |||
| /-- | |||
| `show t` finds the first goal whose target unifies with `t`. It makes that the main goal, | |||
| performs the unification, and replaces the target with the unified version of `t`. | |||
| `show t` declares that the current goal is `t`. | |||
There was a problem hiding this comment.
This could be expanded a bit; it's unclear from this description if this is just a check with no effect if successful, or if it actually changes the goal (as it does). And maybe somewhere uses the verb “unify” to hint that show _ < _ for example works.
There was a problem hiding this comment.
One question: In its current state, show is basically a weaker version of change, right? I feel like instead of changing the documentation and making it officially just a weaker change, we should rather change show to what it's supposed to do from its documentation.
There was a problem hiding this comment.
I actually don't know, so looking forward to reading about it here :-)
There was a problem hiding this comment.
The documentation of change implies this: "The tactic show e is interchangeable with change e, where the pattern e is applied to the main goal." I'd be happy though to make a PR that fixes show (that would imply adding a new @[builtin_tactic] and thus a stage0 update though)
There was a problem hiding this comment.
Sorry, I'm a bit lost. What would you fix beyond the docstring?
There was a problem hiding this comment.
Change show such that it finds the first goal whose target unifies with t, makes that the main goal, performs the unification, and replaces the target with the unified version of t?
There was a problem hiding this comment.
And in such a way that if it applies to the main goal, it behaves exactly like change
There was a problem hiding this comment.
Ah, I see, make it behave like in lean3. I'm sympathetic, but given that users didn't mind that much so far, unsure. I'll let those with more expertise in the tactic language design weigh in.
There was a problem hiding this comment.
I’m not familiar enough with the show tactic to offer a detailed, accurate description beyond what’s already suggested in the original PR. If anyone is interested in taking ownership of this PR or can provide a snippet to include, I would appreciate the help.
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
After discussing this, it seems rather better to adjust the behavior to match the documentation. There is already a draft at #7395. |
|
Even better! Thanks! |
No description provided.