Commit 2023-06-04 11:07 5f25c089

chore(archive/imo): change namespace imo to imoYYYY_qX (#19152) This PR fixes a mistake that I made when namespacing files in archive.imo. Now, the files whose namespace was imo have namespace their file name (minus .lean). Changes:

• namespace imo changed to imoYYYY_qX;
• added nolint dup_namespace tags to the declarations that have a duplication;
• changed namespace imo_1987_q1 to imo1987_q1 for consistency. Zulip discussion