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

Document options --prop, --guarded, and --two-level. #6257

Closed
andreasabel opened this issue Oct 29, 2022 · 3 comments
Closed

Document options --prop, --guarded, and --two-level. #6257

andreasabel opened this issue Oct 29, 2022 · 3 comments
Assignees
@andreasabel
Labels
2ltt Issues related to two-level type theory guarded cubical Guarded Cubical Agda prop Prop, definitional proof irrelevance user-manual Concerning the user manual (sublabel of documentation) ux: documentation Issues relating to Agda's documentation
Milestone
2.6.3

Comments

@andreasabel
Copy link
Member

@nad writes in #6049 (comment):

No, some are missing, including at least --prop, --guarded, and --two-level.

These options should be documented in the user manual.
@andreasabel andreasabel added ux: documentation Issues relating to Agda's documentation user-manual Concerning the user manual (sublabel of documentation) labels Oct 29, 2022
@andreasabel andreasabel added this to the 2.6.3 milestone Oct 29, 2022
@andreasabel andreasabel self-assigned this Oct 29, 2022
@andreasabel andreasabel changed the title Document options --prop Document options --prop, --guarded, and --two-level. Oct 29, 2022
@andreasabel andreasabel added prop Prop, definitional proof irrelevance 2ltt Issues related to two-level type theory guarded cubical Guarded Cubical Agda labels Oct 29, 2022
andreasabel added a commit that referenced this issue Oct 29, 2022
@andreasabel
Fix #6257: doc: add --guarded --prop --two-level to cmd line opts
12afd3b
@andreasabel andreasabel mentioned this issue Oct 29, 2022
Closed
@nad
Copy link
Contributor

nad commented Oct 30, 2022

I found two more undocumented options: --keep-covering-clauses, --lossy-unification.

@nad nad reopened this Oct 30, 2022
@andreasabel
Copy link
Member Author

andreasabel commented Oct 31, 2022 •
edited
Loading

I agree these should also be documented, so feel free to open a new issue. (But I achieved what I set out to do in this issue.)

@nad
Copy link
Contributor

nad commented Oct 31, 2022

See #6269.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
2ltt Issues related to two-level type theory guarded cubical Guarded Cubical Agda prop Prop, definitional proof irrelevance user-manual Concerning the user manual (sublabel of documentation) ux: documentation Issues relating to Agda's documentation
Projects
None yet
Milestone
2.6.3
Development

Successfully merging a pull request may close this issue.

#6257: doc: add --guarded --prop --two-level to cmd line opts agda/agda
2 participants
@nad @andreasabel