feat: lemmas for ReaderT and StateT #373
Merged
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
fgdorais
added
the
awaiting-review
semorrison
reviewed
Nov 20, 2023
Std/Control/Lemmas.lean
Outdated
Comment on lines
7
to
8
| @[simp] theorem run_failure [Monad m] [Alternative m] (ctx : ρ) : | ||
| (failure : ReaderT ρ m α).run ctx = failure := rfl |
There was a problem hiding this comment.
As far as I can tell the naming conventions as written are silent on whether this should be run_failure or failure_run.
I think we should start becoming more consistent about this, and really hope that we can go with failure_run here:
- We all use dot notation, and basic principle is "important fragments of the statement, read left to right".
- This is obviously a theorem about
failuremore than it is a theorem aboutrun, sofailuredeserves top billing.
Obviously we should not hold up this PR for such a discussion, of course. :-)
There was a problem hiding this comment.
The last time this came up, we ended up with "mostly prefix, but binary operators are infix" for a not-completely-defined notion of what constitutes a binary operator. Here run could conceivably be interpreted as a binary operator, but I lean toward not doing so because it doesn't have an associated notation.
semorrison
approved these changes
Nov 20, 2023
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.
Handy lemmas extracted from #85 before closing that old PR.