leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 298 forks source link

[Merged by Bors] - chore(*): add mathlib4 synchronization comments #19239

Closed github-actions[bot] closed 1 year ago

github-actions[bot] commented 1 year ago

Regenerated from the port status wiki page. Relates to the following files:


The following files have no module docstring, so I have not added a message in this PR

Please make a PR to add a module docstring (for Lean3 and Lean4!), then I will add the freeze comment next time.


The following files no longer exist in Lean 3' mathlib, so I have not added a message in this PR

In future we should find where they moved to, and check that the files are still in sync.


I am a bot; please check that I have not put a comment in a bad place before running bors merge!

eric-wieser commented 1 year ago

bors merge

bors[bot] commented 1 year ago

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.