-
Notifications
You must be signed in to change notification settings - Fork 58
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
Missing functionality: impossibility assertions in pattern-matching anonymous functions #275
Comments
I think this is because the If you're blocked on this, here's a work-around: import Decidable.Equality
data MyDATA = ABC | DEF
DecEq MyDATA where
decEq ABC ABC = Yes Refl
decEq ABC DEF = No $ \case Refl impossible
decEq DEF ABC = No $ \case Refl impossible
decEq DEF DEF = Yes Refl |
vfrinken
changed the title
DecEq for data types
Missing functionality: impossibility assertions in pattern-matching anonymous functions
Apr 11, 2020
Worth noting we have lambda-case thanks to #244 |
Thanks! I guess we should decide on whether this is a missing feature, or |
I would argue that lambda case is a good way to go. Especially, if it is well documented. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!
Steps to Reproduce
Expected Behavior
type checking without problems
Idris: File loaded successfully
like Idris 1
Observed Behavior
Parse error: Not the end of a block entry (next tokens: [symbol (, symbol \, identifier Refl, impossible, symbol ), identifier decEq, identifier DEF, identifier ABC, symbol =, identifier No])
The text was updated successfully, but these errors were encountered: