[Merged by Bors] - feat(measure_theory/pmf): lawful monad instance for probability mass function monad #15066
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
… for probability mass function monad
dtumad
added
the
awaiting-review
eric-wieser
reviewed
Jul 6, 2022
src/measure_theory/probability_mass_function/constructions.lean
Outdated
Show resolved
Hide resolved
eric-wieser
reviewed
Jul 6, 2022
| noncomputable theory | ||
| variables {α β γ : Type*} | ||
| variables {α : Type*} {β : Type*} {γ : Type*} |
There was a problem hiding this comment.
Note that this means exactly the same thing as what was written before, so there's no need to change it
There was a problem hiding this comment.
Just changed this to match the other pmf files, probably doesn't matter much I guess. Changed it to switch them all to the simple version
eric-wieser
reviewed
Jul 6, 2022
eric-wieser
added
easy
dtumad
added
awaiting-review
|
@eric-wieser Is this good to be merged? |
eric-wieser
reviewed
Jul 12, 2022
|
✌️ dtumad can now approve this pull request. To approve and merge a pull request, simply reply with |
eric-wieser
added
the
awaiting-CI
leanprover-community-bot-assistant
added
delegated
github-actions
bot
removed
the
awaiting-CI
|
If you want to rerun CI, just click on "Details" to the right of the failed job, and there will be a "Re-run jobs" button (as in this page for the commit 9cd2290), and you may opt to re-run only failed jobs. |
|
You can also use bors merge |
github-actions
bot
added
the
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jul 13, 2022
…function monad (#15066) Provide `is_lawful_functor` and `is_lawful_monad` instances for `pmf`. Also switch the `seq` and `map` operations to the ones coming from the `monad` instance. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Build failed (retrying...): |
bors bot
pushed a commit
that referenced
this pull request
Jul 13, 2022
…function monad (#15066) Provide `is_lawful_functor` and `is_lawful_monad` instances for `pmf`. Also switch the `seq` and `map` operations to the ones coming from the `monad` instance. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
|
@eric-wieser @alreadydone Thanks that's very helpful to know for the future |
joelriou
pushed a commit
that referenced
this pull request
Jul 23, 2022
…function monad (#15066) Provide `is_lawful_functor` and `is_lawful_monad` instances for `pmf`. Also switch the `seq` and `map` operations to the ones coming from the `monad` instance. Co-authored-by: Eric Wieser <wieser.eric@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.
Provide
is_lawful_functorandis_lawful_monadinstances forpmf. Also switch theseqandmapoperations to the ones coming from themonadinstance.This required changing some universe levels to match the way they are in the monad api. I don't think the more general case is generally useful, so I don't think this should be a problem.