Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(tactic/simps): some improvements (#5541)
* `@[simps]` would previously fail if the definition is not a constructor application (with the suggestion to add option `{rhs_md := semireducible}` and maybe `simp_rhs := tt`). Now it automatically adds `{rhs_md := semireducible, simp_rhs := tt}` whenever it reaches this situation. * Remove all (now) unnecessary occurrences of `{rhs_md := semireducible}` from the library. There are still a couple left where the `simp_rhs := tt` is undesirable. * `@[simps {simp_rhs := tt}]` now also applies `dsimp, simp` to the right-hand side of the lemmas it generates. * Add some `@[simps]` in `category_theory/limits/cones.lean` * `@[simps]` would not recursively apply projections of `prod` or `pprod`. This is now customizable with the `not_recursive` option. * Add an option `trace.simps.debug` with some debugging information.
- Loading branch information
1 parent
78d5bd3
commit 12921e9
Showing
39 changed files
with
218 additions
and
184 deletions.
There are no files selected for viewing
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 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 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 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 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 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 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 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 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 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 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
Oops, something went wrong.