Skip to content

doc: rewrite apply?, exact?, rw? and by? docstrings #15008

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.

Sign up for GitHub

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

Open
Vierkantor wants to merge 1 commit into
base: master
Choose a base branch
from
+34 −28
Open

doc: rewrite apply?, exact?, rw? and by? docstrings #15008

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
62 changes: 34 additions & 28 deletions src/Init/Tactics.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1829,31 +1829,38 @@ structure LibrarySearchConfig where
all : Bool := false

/--
Searches environment for definitions or theorems that can solve the goal using `exact`
with conditions resolved by `solve_by_elim`.

The optional `using` clause provides identifiers in the local context that must be
used by `exact?` when closing the goal. This is most useful if there are multiple
ways to resolve the goal, and one wants to guide which lemma is used.

Use `+grind` to enable `grind` as a fallback discharger for subgoals.
Use `+try?` to enable `try?` as a fallback discharger for subgoals.
Use `-star` to disable fallback to star-indexed lemmas (like `Empty.elim`, `And.left`).
Use `+all` to collect all successful lemmas instead of stopping at the first.
`exact?` searches the environment for definitions or theorems that solve the goal using `exact`,
with all side conditions resolved by `solve_by_elim`. After printing the suggestions,
`exact?` closes the current goal with `sorry`. `exact?` is a proof writing tool that should not be
left in finished code.

* `exact? using h₁, ... hₙ` requires that the local hypotheses `h₁`, ..., `hₙ` are
used by `exact?` when closing the goal. This is most useful if there are multiple
ways to resolve the goal, and one wants to guide which lemma is used.
* `exact? (config := cfg)` specifies the configuration using `cfg : LibrarySearchConfig`.
In particular:
* `exact? +grind` enables `grind` as a fallback discharger for subgoals.
* `exact? +try?` enables `try?` as a fallback discharger for subgoals.
* `exact? -star` disables fallback to star-indexed lemmas (like `Empty.elim`, `And.left`).
* `exact? +all` collects all successful lemmas instead of stopping at the first.
-/
syntax (name := exact?) "exact?" optConfig (" using " (colGt ident),+)? : tactic

/--
Searches environment for definitions or theorems that can refine the goal using `apply`
with conditions resolved when possible with `solve_by_elim`.

The optional `using` clause provides identifiers in the local context that must be
used when closing the goal.
`apply?` searches the environment for definitions or theorems that solve the goal using `apply`,
possibly with side conditions resolved by `solve_by_elim`. After printing the suggestions,
`apply?` closes the current goal with `sorry`. `apply?` should not be left in finished code;
it is a search tool.

Use `+grind` to enable `grind` as a fallback discharger for subgoals.
Use `+try?` to enable `try?` as a fallback discharger for subgoals.
Use `-star` to disable fallback to star-indexed lemmas.
Use `+all` to collect all successful lemmas instead of stopping at the first.
* `apply? using h₁, ... hₙ` requires that the local hypotheses `h₁`, ..., `hₙ` are
used by `apply?` when closing the goal. This is most useful if there are multiple
ways to resolve the goal, and one wants to guide which lemma is used.
* `apply? (config := cfg)` specifies the configuration using `cfg : LibrarySearchConfig`.
In particular:
* `apply? +grind` enables `grind` as a fallback discharger for subgoals.
* `apply? +try?` enables `try?` as a fallback discharger for subgoals.
* `apply? -star` disables fallback to star-indexed lemmas (like `Empty.elim`, `And.left`).
* `apply? +all` collects all successful lemmas instead of stopping at the first.
-/
syntax (name := apply?) "apply?" optConfig (" using " (colGt term),+)? : tactic

Expand All @@ -1863,13 +1870,12 @@ Syntax for excluding some names, e.g. `[-my_lemma, -my_theorem]`.
syntax rewrites_forbidden := " [" (("-" ident),*,?) "]"

/--
`rw?` tries to find a lemma which can rewrite the goal.

`rw?` should not be left in proofs; it is a search tool, like `apply?`.

Suggestions are printed as `rw [h]` or `rw [← h]`.
`rw?` searches the environment for lemmas which can rewrite the goal. After printing the suggestions,
`rw?` applies the first, most specific result. Suggestions are printed as `rw [h]` or `rw [← h]`.
`rw?` should not be left in finished code; it is a search tool.

You can use `rw? [-my_lemma, -my_theorem]` to prevent `rw?` using the named lemmas.
* `rw? at loc` tries to rewrite at location(s) `loc`.
* `rw? [-my_lemma, -my_theorem]` prevents `rw?` from using the named lemmas as suggestions.
-/
syntax (name := rewrites?) "rw?" (ppSpace location)? (rewrites_forbidden)? : tactic

Expand All @@ -1889,8 +1895,8 @@ macro (name := showTermElab) tk:"show_term " t:term : term =>
`(term| no_implicit_lambda% (show_term_elab%$tk $t))

/--
The command `by?` will print a suggestion for replacing the proof block with a proof term
using `show_term`.
`by? tacs` runs the tactic sequence `tacs` and suggests to replace the `by?` block with the proof
term generated by the tactics.
-/
macro (name := by?) tk:"by?" t:tacticSeq : term => `(show_term%$tk by%$tk $t)

Expand Down
Loading