[Merged by Bors] - feat(library/init/meta/tactic): informative tactic combinators #212
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
Most of the combinators for tactics (e.g. `focus`, `all_goals`, `solve`) used to work only with `tactic unit`s. This commit adds 'informative' variants of these combinators which work with general `tactic α`.
… tactic combinators In 94e1dcb, we added 'informative' variants of tactic combinators like `all_goals` and `focus`. These were previously called `all_goals'`, `focus'` etc. However, this is inconsistent with the existing naming convention for `mmap`/`mmap'` etc., where the non-informative variant (i.e. the one working with `tactic unit` only) gets the prime. This commit therefore swaps the naming convention for the tactic combinators.
|
bors merge |
bors bot
pushed a commit
that referenced
this pull request
May 11, 2020
Many tactic combinators currently only work with `tactic unit`s. This PR introduces variants of these combinators which work with general `tactic α`s, as suggested in #206. This is a choose-your-own-PR: It contains two commits corresponding to two different designs from #206. The first commit is more conservative: it leaves the existing combinators alone and implements the new ones with primed names (`all_goals'` etc). This leads to no breakage in core and very minimal breakage in mathlib. The second commit switches the names around so that the `unit`-valued combinators get the prime. This leads to mild breakage in core/mathlib, but is more consistent with the existing naming conventions (e.g. `mmap` vs `mmap'`). I'd prefer that both commits get merged, but if you want just the first one, that's also fine by me. fixes #206
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
bors bot
pushed a commit
to leanprover-community/mathlib
that referenced
this pull request
May 15, 2020
## Changes to bracket notation
* `{a}` now requires an instance `has_singleton`;
* `insert a ∅ = {a}` is called `insert_emptyc_eq`, provided by an `is_lawful_singleton` instance;
* `a ∈ ({b} : set α)` is now defeq `a = b`, not `a = b ∨ false`;
* `({a} : set α)` is no longer defeq `insert a ∅`;
* `({a} : finset α)` now means `⟨⟨[a]⟩, _⟩` (used to be called `finset.singleton a`), not `insert a ∅`;
* removed `finset.singleton`;
* `{a, b}` is now `insert a {b}`, not `insert b {a}`.
* `finset.univ : finset bool` is now `{tt, ff}`;
* `(({a} : finset α) : set α)` is no longer defeq `{a}`.
## Tactic `norm_num`
The interactive tactic `norm_num` was recently rewritten in Lean. The non-interactive `tactic.norm_num` has been removed in Lean 3.12 so that we can migrate the algebraic hierarchy to mathlib in 3.13.
## Tactic combinators
leanprover-community/lean#212 renames a bunch of tactic combinators. We change to using the new names.
## Tactic `case`
leanprover-community/lean#228 slightly changes the semantics of the `case` tactic. We fix the resulting breakage to be conform the new semantics.
Co-authored-by: Jannis Limperg <jannis@limperg.de>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this pull request
May 16, 2020
## Changes to bracket notation
* `{a}` now requires an instance `has_singleton`;
* `insert a ∅ = {a}` is called `insert_emptyc_eq`, provided by an `is_lawful_singleton` instance;
* `a ∈ ({b} : set α)` is now defeq `a = b`, not `a = b ∨ false`;
* `({a} : set α)` is no longer defeq `insert a ∅`;
* `({a} : finset α)` now means `⟨⟨[a]⟩, _⟩` (used to be called `finset.singleton a`), not `insert a ∅`;
* removed `finset.singleton`;
* `{a, b}` is now `insert a {b}`, not `insert b {a}`.
* `finset.univ : finset bool` is now `{tt, ff}`;
* `(({a} : finset α) : set α)` is no longer defeq `{a}`.
## Tactic `norm_num`
The interactive tactic `norm_num` was recently rewritten in Lean. The non-interactive `tactic.norm_num` has been removed in Lean 3.12 so that we can migrate the algebraic hierarchy to mathlib in 3.13.
## Tactic combinators
leanprover-community/lean#212 renames a bunch of tactic combinators. We change to using the new names.
## Tactic `case`
leanprover-community/lean#228 slightly changes the semantics of the `case` tactic. We fix the resulting breakage to be conform the new semantics.
Co-authored-by: Jannis Limperg <jannis@limperg.de>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
cipher1024
pushed a commit
to cipher1024/mathlib
that referenced
this pull request
Mar 15, 2022
## Changes to bracket notation
* `{a}` now requires an instance `has_singleton`;
* `insert a ∅ = {a}` is called `insert_emptyc_eq`, provided by an `is_lawful_singleton` instance;
* `a ∈ ({b} : set α)` is now defeq `a = b`, not `a = b ∨ false`;
* `({a} : set α)` is no longer defeq `insert a ∅`;
* `({a} : finset α)` now means `⟨⟨[a]⟩, _⟩` (used to be called `finset.singleton a`), not `insert a ∅`;
* removed `finset.singleton`;
* `{a, b}` is now `insert a {b}`, not `insert b {a}`.
* `finset.univ : finset bool` is now `{tt, ff}`;
* `(({a} : finset α) : set α)` is no longer defeq `{a}`.
## Tactic `norm_num`
The interactive tactic `norm_num` was recently rewritten in Lean. The non-interactive `tactic.norm_num` has been removed in Lean 3.12 so that we can migrate the algebraic hierarchy to mathlib in 3.13.
## Tactic combinators
leanprover-community/lean#212 renames a bunch of tactic combinators. We change to using the new names.
## Tactic `case`
leanprover-community/lean#228 slightly changes the semantics of the `case` tactic. We fix the resulting breakage to be conform the new semantics.
Co-authored-by: Jannis Limperg <jannis@limperg.de>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
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.
Many tactic combinators currently only work with
tactic units. This PR introduces variants of these combinators which work with generaltactic αs, as suggested in #206.This is a choose-your-own-PR: It contains two commits corresponding to two different designs from #206. The first commit is more conservative: it leaves the existing combinators alone and implements the new ones with primed names (
all_goals'etc). This leads to no breakage in core and very minimal breakage in mathlib. The second commit switches the names around so that theunit-valued combinators get the prime. This leads to mild breakage in core/mathlib, but is more consistent with the existing naming conventions (e.g.mmapvsmmap').I'd prefer that both commits get merged, but if you want just the first one, that's also fine by me.
fixes #206