8000 GenericError crusade by andreasabel · Pull Request #7512 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

GenericError crusade #7512

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
Merged
merged 3 commits into from
Sep 26, 2024
Merged

GenericError crusade #7512

merged 3 commits into from
Sep 26, 2024

Conversation

andreasabel
Copy link
Member
  • Refactor: use Set1 Induction in ConstructorName
  • Refactor checkEarlierThan to return False instead of GenericError
  • New error JSBackend.BadCompilePragma and reproducer

@andreasabel andreasabel added ux: error reporting Issues to do with how Agda reports errors GenericError Concerning GenericError and GenericDocError labels Sep 26, 2024
@andreasabel andreasabel added this to the 2.8.0 milestone Sep 26, 2024
@andreasabel andreasabel added the pr: preserve commits PR should be merged via rebase, preserving the commits label Sep 26, 2024
@andreasabel andreasabel self-assigned this Sep 26, 2024
@andreasabel andreasabel merged commit 756b4fb into master Sep 26, 2024
28 checks passed
@andreasabel andreasabel deleted the foo-bar branch September 26, 2024 20:49
@andreasabel andreasabel mentioned this pull request Sep 26, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@andreasabel andreasabel

Labels
GenericError Concerning GenericError and GenericDocError pr: preserve commits PR should be merged via rebase, preserving the commits ux: error reporting Issues to do wi 4835 th how Agda reports errors
Projects
None yet
Milestone
2.8.0
Development

Successfully merging this pull request may close these issues.
1 participant
@andreasabel
0