Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Cubical.**.Foo should only import **.Foo.Base and **.Foo.Properties #396

Open
Saizan opened this issue Aug 3, 2020 · 0 comments
Open

Cubical.**.Foo should only import **.Foo.Base and **.Foo.Properties #396

Saizan opened this issue Aug 3, 2020 · 0 comments
Assignees
@felixwellen
Labels
order Structuring, enforcing conventions, renaming, ...

Comments

@Saizan
Copy link
Contributor

Saizan commented Aug 3, 2020

I think a Foo module should export what you're more likely to need about Foo.

If they re-export everything that's been developed for Foo then they are not as useful to import, as that slows down typechecking from scratch and bring a lot of names into the namespace.

We should also add this policy to CONTRIBUTING.md.
felixwellen added a commit to felixwellen/cubical that referenced this issue May 4, 2022
@felixwellen
WIP: agda#396, enforce rules for imports
aa2ada9
felixwellen added a commit to felixwellen/cubical that referenced this issue May 4, 2022
@felixwellen
WIP: agda#396, enforce rules for imports
171c134
mortberg pushed a commit that referenced this issue May 5, 2022
@felixwellen
Issue #396: enforce import rules (#783)
a8dbd61 
* WIP: #396, enforce rules for imports

* WIP: #396, enforce rules for imports

* more fixed imports

* more fixed imports

* more fixed imports

* kill empty line
@felixwellen felixwellen added order Structuring, enforcing conventions, renaming, ... and removed enhancement labels May 22, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@felixwellen felixwellen

Labels
order Structuring, enforcing conventions, renaming, ...
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@Saizan @ecavallo @felixwellen