You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We aim to have unique identifiers for all public definitions throughout the codebase, as stated in the library coding style guide. This was supposed to be enforced by recursively opening all modules of the library, so that Agda would complain about duplicate definitions when checking the Everything file.
Unfortunately we aren't properly opening the top-level modules, so while we avoided naming collisions inside top-level modules, we managed to introduce duplicates across top-level module boundaries. These should be resolved by either removing one of the definitions, and reusing the other, or by renaming one or both definitions to something less ambiguous.
So far I found the following duplicates:
Theory of finite groups is duplicated between finite-algebra and finite-group-theory. The finite-algebra module should build on top of the formalization from finite-group-theory
foundation.separated-types.is-separated vs orthogonal-factorization-systems.separated-types.is-separated
univalent-combinatorics.standard-finite-types.Fin vs reflection.group-solver.Fin
universal-algebra.terms-over-signatures.Term vs reflections.terms.Term
foundation.path-algebra.cube vs univalent-combinatorics.cubes.cube
The Everything file is generated by a script in the Makefile, so once the duplicates are resolved, we should change the script to generate open import <module> public lines.
The text was updated successfully, but these errors were encountered:
We aim to have unique identifiers for all public definitions throughout the codebase, as stated in the library coding style guide. This was supposed to be enforced by recursively opening all modules of the library, so that Agda would complain about duplicate definitions when checking the Everything file.
Unfortunately we aren't properly opening the top-level modules, so while we avoided naming collisions inside top-level modules, we managed to introduce duplicates across top-level module boundaries. These should be resolved by either removing one of the definitions, and reusing the other, or by renaming one or both definitions to something less ambiguous.
So far I found the following duplicates:
finite-algebra
andfinite-group-theory
. Thefinite-algebra
module should build on top of the formalization fromfinite-group-theory
foundation.separated-types.is-separated
vsorthogonal-factorization-systems.separated-types.is-separated
univalent-combinatorics.standard-finite-types.Fin
vsreflection.group-solver.Fin
universal-algebra.terms-over-signatures.Term
vsreflections.terms.Term
foundation.path-algebra.cube
vsunivalent-combinatorics.cubes.cube
The Everything file is generated by a script in the Makefile, so once the duplicates are resolved, we should change the script to generate
open import <module> public
lines.The text was updated successfully, but these errors were encountered: