[Merged by Bors] - chore(*): update to Lean-3.35.0c #9988
Conversation
|
@gebner What are the two new types called stream in Lean 4? |
urkud
changed the title
stream from core to mathlib
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Leonardo de Moura | ||
| -/ | ||
|
|
There was a problem hiding this comment.
Can you add a brief comment explaining why this is called init? I assume the reason is "it used to be part of the prelude"?
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Leonardo de Moura | ||
| -/ | ||
|
|
There was a problem hiding this comment.
Similarly in this file, it would be nice to explain the choice of init in the filename.
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
There was a problem hiding this comment.
bors d+
I didn't check that the new files match the ones copied from core, I trust your copy pasting!
Can you add a comment to the PR description explaining the choice of init.lean filenames (and mention if these used to be part of the prelude but are no longer), and similarly add a comment to that end in each of the init.lean files?
github-actions
bot
added
delegated
|
bors r+ |
github-actions
bot
added
the
ready-to-merge
Move `stream`, `rbtree`, and `rbmap` from core to `mathlib` and reflows some long lines. Rename some files to avoid name clashes.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Move `stream`, `rbtree`, and `rbmap` from core to `mathlib` and reflows some long lines. Rename some files to avoid name clashes.
Move
stream,rbtree, andrbmapfrom core tomathliband reflows some long lines. Rename some files to avoid name clashes.