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] - feat: port Data.Seq.Computation #1216
Conversation
This should probably be |
Makes sense -- I'll hold until after we get resolution for the last issue, and then rename. |
lake-manifest.json
Outdated
@@ -37,18 +37,6 @@ | |||
"rev": "72610cec1cd686884a08704f5fa91b45262136f9", | |||
"name": "aesop", | |||
"inputRev?": "master"}}, | |||
{"git": |
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.
Why are these changes being made in this PR?
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.
They should not be -- this was in error.
|
ab28668
to
6d802a7
Compare
Sorry, I made a mess out of the git history. I "fixed" it using a force push that squashes all the changes into 1 commit. |
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
a4e6552
to
09db318
Compare
Thanks 🎉 bors merge |
Port of data.seq.computation Requires renaming `return` to `pure` Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded:
|
Port of data.seq.computation
Requires renaming
return
topure