Closed VictorTaelin closed 21 hours ago
Base//ALL.agda: exports everything in Base/
Base/ALL.agda: exports everything in Base
Note: we should NEVER import ALL inside Base. Instead, this is for libraries and apps OUTSIDE of Base, that import it.
I've also changed some Ord files, and how the Pair module works.
Base//ALL.agda: exports everything in Base/
Base/ALL.agda: exports everything in Base
Note: we should NEVER import ALL inside Base. Instead, this is for libraries and apps OUTSIDE of Base, that import it.
I've also changed some Ord files, and how the Pair module works.