8000 New unstructured error `IdiomBracketError` by andreasabel · Pull Request #7461 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

New unstructured error IdiomBracketError #7461

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

Merged
merged 1 commit into from
Aug 31, 2024
Merged

Conversation

andreasabel
Copy link
Member
@andreasabel andreasabel commented Aug 29, 2024

Replacing some uses of GenericError.

There are 4 error conditions for IdiomBracketError which one could make named sub-errors of IdiomBracketError, but saved myself the effort because I consider the feature fringe:

2 of the error conditions were already covered by the testsuite, this PR adds the 2 missing reproducers.

Replacing some uses of `GenericError`.
@andreasabel andreasabel added idiom brackets Desugaring and checking of idiom brackets GenericError Concerning GenericError and GenericDocError labels Aug 29, 2024
@andreasabel andreasabel added this to the 2.8.0 milestone Aug 29, 2024
@andreasabel andreasabel self-assigned this Aug 29, 2024
@andreasabel andreasabel added the infra: test suite Issues relating to the test suite (not in changelog) label Aug 31, 2024
@andreasabel andreasabel merged commit 693c7ef into master Aug 31, 2024
28 checks passed
@andreasabel andreasabel deleted the idiom-bracket-errors branch August 31, 2024 07:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
GenericError Concerning GenericError and GenericDocError idiom brackets Desugaring and checking of idiom brackets infra: test suite Issues relating to the test suite (not in changelog)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant
0