mathlib3
ddfa266e - feat: add warning to scripts/port_status.py (#17132)

Commit
3 years ago
feat: add warning to scripts/port_status.py (#17132) Adds some warnings about work that needs to be done to keep tracking of porting, e.g. ``` # The following files are marked as ported, but do not have a SYNCHRONIZED WITH MATHLIB4 label. logic.is_empty data.fin.fin2 data.sigma.basic # The following files are marked as ported, but have not been verified against a commit hash from mathlib. logic.is_empty data.fin.fin2 algebra.abs algebra.covariant_and_contravariant algebra.group.basic algebra.group.defs # The following files have been modified since the commit at which they were verified. logic.relator ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading