Open github-actions[bot] opened 1 year ago
Regenerated from the port status wiki page. Relates to the following files:
algebraic_topology.dold_kan.equivalence
algebraic_topology.dold_kan.equivalence_pseudoabelian
combinatorics.quiver.covering
linear_algebra.quadratic_form.dual
The following files have no module docstring, so I have not added a message in this PR
control.basic
control.monad.cont
control.monad.writer
control.traversable.derive
data.array.lemmas
data.bitvec.basic
data.buffer.basic
data.rbmap.basic
data.rbmap.default
data.rbtree.basic
data.rbtree.default_lt
data.rbtree.find
data.rbtree.init
data.rbtree.insert
data.rbtree.main
data.rbtree.min_max
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
data.buffer.parser
data.dlist
data.vector
init.algebra.classes
init.algebra.functions
init.algebra.order
init.control.lawful
init.data.int.bitwise
init.data.int.comp_lemmas
init.data.list.instances
init.data.list.lemmas
init.data.nat.bitwise
init.data.nat.gcd
init.data.nat.lemmas
init.data.ordering.lemmas
init.data.sigma.lex
init.data.subtype.basic
init.function
init.ite_simp
init.meta.well_founded_tactics
oxford_invariants.«2021summer».week3_p1
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!
bors merge
Regenerated from the port status wiki page. Relates to the following files:
algebraic_topology.dold_kan.equivalence
algebraic_topology.dold_kan.equivalence_pseudoabelian
combinatorics.quiver.covering
linear_algebra.quadratic_form.dual
The following files have no module docstring, so I have not added a message in this PR
control.basic
control.monad.cont
control.monad.writer
control.traversable.derive
data.array.lemmas
data.bitvec.basic
data.buffer.basic
data.rbmap.basic
data.rbmap.default
data.rbtree.basic
data.rbtree.default_lt
data.rbtree.find
data.rbtree.init
data.rbtree.insert
data.rbtree.main
data.rbtree.min_max
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
data.buffer.parser
data.dlist
data.vector
init.algebra.classes
init.algebra.functions
init.algebra.order
init.control.lawful
init.data.int.bitwise
init.data.int.comp_lemmas
init.data.list.instances
init.data.list.lemmas
init.data.nat.bitwise
init.data.nat.gcd
init.data.nat.lemmas
init.data.ordering.lemmas
init.data.sigma.lex
init.data.subtype.basic
init.function
init.ite_simp
init.meta.well_founded_tactics
oxford_invariants.«2021summer».week3_p1
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
!