Does anyone know why Idris 2 can’t figure this out? I have to explicitly tell it that xs matches _::_, even though it knows xs can’t match Nil (because it’s in the wrong case)
(This also happens with case..of)
read image description
ALT
1
1
3
Conversation
The simplest answer is just “it isn’t that smart” but I’m wondering if there’s a more detailed answer explaining whys
2
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Is this a major implementation barrier, or one that’s really just more convenient?
3
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
