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
Looks similar to the ‘forced patterns’ feature was working on for Aya?
For this specific issue, you might need to help Idris along by matching on the implicit `n` parameter. This might let you remove the redundant case. twitter.com/OwoTizusa/stat
This Tweet is unavailable.
2
2
I think I’ve seen the removal of impossible cases referred to as ‘pruning’ in the past. But could be wrong!
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Show replies