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.

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

[ new ] Quantity for proof in with-clauses #3415

Open
wants to merge 3 commits into
base: main
Choose a base branch
from

Conversation

spcfox
Copy link
Contributor

@spcfox spcfox commented Nov 18, 2024

Description

Currently the quantity of proof in with-clause is the same as the quantity of expression. But often proofs are needed only at compile time. Example:

filterSquared : (p : a -> Bool) -> (xs : List a) ->
                filter p (filter p xs) === filter p xs
filterSquared p [] = Refl
filterSquared p (x :: xs) with (p x) proof 0 eq
  filterSquared p (x :: xs) | False = filterSquared p xs
  filterSquared p (x :: xs) | True
    = rewrite eq in cong (x ::) (filterSquared p xs)

So I suggest adding the ability to separately specify quantities for proofs.

Note that prf is currently erased in the following code, but in this version it will now be unrestricted, as will all variables for which multiplicity is not explicitly specified. This may affect existing code and probably requires discussion.

foo x with 0 (x) proof prf

Should this change go in the CHANGELOG?

  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md (and potentially also
    CONTRIBUTORS.md).

src/Idris/REPL.idr Outdated Show resolved Hide resolved
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant