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

Implicitly import SSet from Agda.Primitive along with Prop & Set #6634

Merged
merged 1 commit into from
May 13, 2023
Merged

Implicitly import SSet from Agda.Primitive along with Prop & Set #6634

merged 1 commit into from
May 13, 2023

Conversation

andreasabel
Copy link
Member

Without any explicit imports, Set and Prop are in scope, but not SSet which requires open Agda.Primitive.

This patch rectifies this and puts SSet on par with Set and Prop.

@andreasabel andreasabel added import Issues to do with importing modules sorts Agda's sort system (see also piSort); univSort; Sort metas; Fibrancy 2ltt Issues related to two-level type theory labels May 13, 2023
@andreasabel andreasabel added this to the 2.6.4 milestone May 13, 2023
@jespercockx
Copy link
Member

Is this a desirable change? The main reason why Set and Prop are imported automatically is because of backwards compatibility (and also because they are widely used, or at least Set is). Neither of those seem to be an issue for SSet at the moment, so I would caution against polluting the user namespace.

@jespercockx
Copy link
Member

Perhaps a better change would be to allow a .agda-lib file to specify a "prelude" module that is imported implicitly in all its modules.

@andreasabel
Implicitly import SSet for --two-level from Agda.Primitive
22714ea 
With `--import-sorts`, `SSet` is now in scope if `--two-level` is given, and `Prop` only if `--prop` is given.

Previously, without any explicit imports, `Set` and `Prop` were in scope, but not `SSet` which required `open Agda.Primitive`.
@andreasabel
Copy link
Member Author

Followed @plt-amy 's oral review and guarded the import of Prop under --prop as well as SSet under --two-level.

@andreasabel andreasabel self-assigned this May 13, 2023
@andreasabel andreasabel merged commit fd0ef9f into master May 13, 2023
33 checks passed
@andreasabel andreasabel deleted the import-SSet branch May 13, 2023 15:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@plt-amy plt-amy Awaiting requested review from plt-amy

@jespercockx jespercockx Awaiting requested review from jespercockx

Assignees

@andreasabel andreasabel

Labels
2ltt Issues related to two-level type theory import Issues to do with importing modules sorts Agda's sort system (see also piSort); univSort; Sort metas; Fibrancy
Projects
None yet
Milestone
2.6.4
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@andreasabel @jespercockx