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

Sized warning #55

Merged
merged 4 commits into from
Jul 4, 2024
Merged

Sized warning #55

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e087b89
extend note on sized types
pmbittner Jul 3, 2024
8cfbe04
delete deprecated SizeJuggle file
pmbittner Jul 3, 2024
6ffe856
README: Provide a more general link for sized types inconsistencies
ibbem Jul 3, 2024
8f2839e
README: refine reasoning on sized types
pmbittner Jul 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -390,9 +390,10 @@ Proofs are documented inline via comments in the code (also see the Documentatio

#### On Axioms and Assumptions

We use sized types, which currently have [known inconsistencies](https://github.com/agda/agda/issues/6002), for termination checking.
For termination checking, we use sized types, which currently have [known inconsistencies](https://github.com/agda/agda/issues/6002).
pmbittner marked this conversation as resolved.
Show resolved Hide resolved
The risks of using them in inconsistent ways are [often accepted](https://github.com/agda/agda/issues/4908) because they can simplify proofs substantially.
We came to the same conclusion and tried our best to use them without interaction with more complicated language features to reduce the likelihood of encountering an inconsistency.
(In particular, we only use the plain inductive flavor `Size` with `↑_` and do not mix it with the `Size<_` type because it is especially mixing the two which is causing inconsistencies (in particular in case of the issue above).)
ibbem marked this conversation as resolved.
Show resolved Hide resolved

Our library, does not use any of the following assumptions or axioms in central parts of the code:

Expand Down
183 changes: 0 additions & 183 deletions src/Util/SizeJuggle.agda
View file
Open in desktop

This file was deleted.

Loading