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.

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

Document --two-level #5868

Closed
nad opened this issue Apr 22, 2022 · 3 comments · Fixed by #6340
Closed

Document --two-level #5868

nad opened this issue Apr 22, 2022 · 3 comments · Fixed by #6340
Labels
2ltt Issues related to two-level type theory help wanted type: enhancement Issues and pull requests about possible improvements ux: documentation Issues relating to Agda's documentation
Milestone

Comments

@nad
Copy link
Contributor

nad commented Apr 22, 2022

The flag --two-level is not mentioned in the documentation.

@nad nad added type: enhancement Issues and pull requests about possible improvements ux: documentation Issues relating to Agda's documentation 2ltt Issues related to two-level type theory labels Apr 22, 2022
@nad nad added this to the 2.6.3 milestone Apr 22, 2022
@jespercockx jespercockx modified the milestones: 2.6.3, later Aug 31, 2022
@mikeshulman
Copy link
Contributor

As of #6258 its existence is at least mentioned. But apparently it is still not described anywhere.

@andreasabel
Copy link
Member

Maybe it was too experimental, so the contributors didn't give it citizen rights. But since it is still here, would be nice if someone volunteered a documentation.

@mikeshulman
Copy link
Contributor

It's probably a bit more stable than it was originally, now that a few of us have started actually using it and some bugs have been reported and fixed. And other experimental options do appear in the reference manual.

However, it would still be nice if something could be done about #5761, particularly the point about the empty type here that doesn't actually involve cumulativity (should I report that as a separate bug?).

andreasabel added a commit that referenced this issue Nov 19, 2022
Fixes #5868. Article by ElifUskuplu.

Co-authored-by: ElifUskuplu <77177090+ElifUskuplu@users.noreply.github.com>
andreasabel added a commit that referenced this issue Nov 19, 2022
Fixes #5868. Article by ElifUskuplu.

Co-authored-by: ElifUskuplu <77177090+ElifUskuplu@users.noreply.github.com>
@andreasabel andreasabel modified the milestones: later, 2.6.3 Nov 22, 2022
@asr asr changed the title Document --two-level Document --two-level Jan 23, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
2ltt Issues related to two-level type theory help wanted type: enhancement Issues and pull requests about possible improvements ux: documentation Issues relating to Agda's documentation
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants