Closed github-actions[bot] closed 1 year ago
bors r+
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.
Regenerated from the port status wiki page. Relates to the following files:
algebra.category.Group.subobject
analysis.analytic.composition
analysis.convex.intrinsic
analysis.inner_product_space.two_dim
analysis.special_functions.japanese_bracket
category_theory.differential_object
geometry.euclidean.angle.oriented.basic
measure_theory.function.conditional_expectation.ae_measurable
order.category.BddOrd
order.category.Semilat
ring_theory.polynomial.hermite.basic
ring_theory.polynomial.hermite.gaussian
ring_theory.ring_hom.integral
ring_theory.ring_hom_properties
The following files have no module docstring, so I have not added a message in this PR
control.basic
control.monad.writer
data.bitvec.basic
data.seq.computation
data.seq.parallel
data.seq.seq
data.seq.wseq
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
lean_core.data.vector
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
!