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.
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
[Merged by Bors] - chore: refactor of Algebra/Group/Defs to reduce imports #9606
Conversation
Can you
Personally I'm wondering why you're trying to get rid of
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice work!
For the benefit of future readers, could you also note the changes to Tactic.Basic
in the PR description?
bors d=@YaelDillies
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
From my reading, you're not attached to having injectivity lemmas be in a new file on their own. Therefore could they go in Algebra.Group.Basic
?
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Done. |
a901444
to
14bf968
Compare
bors merge |
We are not that far from the point that `Algebra/Group/Defs` depends on nothing significant besides `simps` and `to_additive`. This removes from `Mathlib.Algebra.Group.Defs` the dependencies on * `Mathlib.Tactic.Basic` (which is a grab-bag of random stuff) * `Mathlib.Init.Algebra.Classes` (which is ancient and half-baked) * `Mathlib.Logic.Function.Basic` (not particularly important, but it is barely used in this file) The goal is to avoid all unnecessary imports to set up the *definitions* of basic algebraic structures. We also separate out `Mathlib.Tactic.TypeStar` and `Mathlib.Tactic.Lemma` as prerequisites to `Mathlib.Tactic.Basic`, but which can be imported separately when the rest of `Mathlib.Tactic.Basic` is not needed. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded: |
open Lean | ||
|
||
/-- `lemma` means the same as `theorem`. It is used to denote "less important" theorems -/ | ||
syntax (name := lemma) declModifiers | ||
group("lemma " declId ppIndent(declSig) declVal Parser.Command.terminationSuffix) : command | ||
|
||
/-- Implementation of the `lemma` command, by macro expansion to `theorem`. -/ | ||
@[macro «lemma»] def expandLemma : Macro := fun stx => | ||
-- FIXME: this should be a macro match, but terminationSuffix is not easy to bind correctly. | ||
-- This implementation ensures that any future changes to `theorem` are reflected in `lemma` | ||
let stx := stx.modifyArg 1 fun stx => | ||
let stx := stx.modifyArg 0 (mkAtomFrom · "theorem" (canonical := true)) | ||
stx.setKind ``Parser.Command.theorem | ||
pure <| stx.setKind ``Parser.Command.declaration |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@semorrison, was moving these declarations to the root namespace (instead of leaving them in Mathlib.Tactic
) deliberate?
We are not that far from the point that
Algebra/Group/Defs
depends on nothing significant besidessimps
andto_additive
.This removes from
Mathlib.Algebra.Group.Defs
the dependencies onMathlib.Tactic.Basic
(which is a grab-bag of random stuff)Mathlib.Init.Algebra.Classes
(which is ancient and half-baked)Mathlib.Logic.Function.Basic
(not particularly important, but it is barely used in this file)The goal is to avoid all unnecessary imports to set up the definitions of basic algebraic structures.
We also separate out
Mathlib.Tactic.TypeStar
andMathlib.Tactic.Lemma
as prerequisites toMathlib.Tactic.Basic
, but which can be imported separately when the rest ofMathlib.Tactic.Basic
is not needed.