Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

chore(*): add mathlib4 synchronization comments #19240

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

github-actions[bot]
Copy link

@github-actions github-actions bot commented Aug 20, 2023

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

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!

@github-actions github-actions bot requested review from a team as code owners August 20, 2023 00:19
@github-actions github-actions bot added awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. mathlib4-synchronization This PR *only* adds a message to the module doc about synchronization with mathlib4 labels Aug 20, 2023
@github-actions github-actions bot force-pushed the create-pull-request/patch branch 2 times, most recently from 41c0b18 to f9282be Compare September 1, 2023 00:20
@github-actions github-actions bot force-pushed the create-pull-request/patch branch 3 times, most recently from df1f954 to 654d707 Compare September 19, 2023 00:19
@YaelDillies YaelDillies removed the request for review from a team September 19, 2023 08:19
@github-actions github-actions bot force-pushed the create-pull-request/patch branch 3 times, most recently from 5ac49dd to 0c9b897 Compare October 12, 2023 00:18
@github-actions github-actions bot force-pushed the create-pull-request/patch branch 2 times, most recently from 95aad47 to 28da11e Compare October 23, 2023 00:20
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. mathlib4-synchronization This PR *only* adds a message to the module doc about synchronization with mathlib4
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant