[Merged by Bors] - doc: Improve Field's fields docstrings#11508
[Merged by Bors] - doc: Improve Field's fields docstrings#11508YaelDillies wants to merge 4 commits intomasterfrom
Field's fields docstrings#11508Conversation
Reduce the diff of #11203
| -- Check that we have not imported `Mathlib.Tactic.Common` yet. | ||
| assert_not_exists Mathlib.Tactic.LibrarySearch.librarySearch |
There was a problem hiding this comment.
seems like a strange way to test for this, especially because something like that might move to Std at some point. (EDIT: nevermind, I see you just pulled this from the bottom of the file. Is there a reason for moving it?)
There was a problem hiding this comment.
The reason is that the content of a file doesn't change whether an assert_not_exists in it succeeds or not, so we might as well put it as early as possible.
I believe @semorrison started by putting them at the end, but eventually decided to put them first.
| Set this to `qsmulRec _` unless there is a risk of a `Module ℚ _` instance diamond. | ||
| Do not use directly. Instead use the `•` notation. -/ |
There was a problem hiding this comment.
I don't think we want to explicitly advocate for the default values.
There was a problem hiding this comment.
Nono, this is not advocating for default values. This is saying that people shouldn't be writing DivisionRing.qsmul q a but q • a
There was a problem hiding this comment.
No, above that it says, "Set this to qsmulRec unless ..."
There was a problem hiding this comment.
Oh, I didn't write that. @eric-wieser just added it in #11262
| instance RatCast.toOfScientific [RatCast K] : OfScientific K where | ||
| ofScientific (m : ℕ) (b : Bool) (d : ℕ) := Rat.ofScientific m b d |
There was a problem hiding this comment.
Not for this PR: is it possible to have an ofScientific instance for ℚ≥0 (or types with an NNRatCast instance)? I guess it would probably require interpreting -1.2 as 1.2.
There was a problem hiding this comment.
I think that would be a big trap. Certainly if people want it they can add it, but I won't do so myself
|
bors merge |
Reduce the diff of #11203
|
Pull request successfully merged into master. Build succeeded: |
Field's fields docstringsField's fields docstrings
Reduce the diff of #11203