Skip to content

Preview: depostulate axioms #1380

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

Open
wants to merge 41 commits into
base: master
Choose a base branch
from

Conversation

fredrik-bakke
Copy link
Collaborator

@fredrik-bakke fredrik-bakke commented Mar 24, 2025

Here's a preview of what the library might look like with depostulated axioms.

Depends on #1373

#1379

@@ -115,7 +115,7 @@ def filter_agda_files(f): return utils.is_agda_file(pathlib.Path(f)) and os.path

temp_dir = 'temp'
status = 0
agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching'
agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching -WnoPatternShadowsConstructor'
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why wouldn't we want these warnings?

Also, is the question of including this pragma orthogonal to the purpose of this pull request, or am I missing something?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I thought this pragma promoted the warning to an error. It is orthogonal to this PR, but not to #1373 on which it depends

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(There it caused errors in the file elementary-number-theory.multiplication-integers)

@fredrik-bakke fredrik-bakke marked this pull request as ready for review March 26, 2025 15:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants