data Even: Nat -> Type where
EvenZ: Even Z
EvenS: Even n -> Even (n + 2)
total
lemma1: Even Z
lemma1 = EvenZ
-- total
-- lemma2: Even Z
-- lemma2 impossible -- Idris says 'lemma2 is a valid case' and I agree with you
total
lemma3: Even 2
lemma3 = EvenS EvenZ
total
lemma4: Even 2 -> Void
lemma4 x impossible -- what does it work?
total
lemma5: Even 1 -> Void
lemma5 x impossible
Я написал несколько доказательств по Even.
lemma1, lemma2 и lemma3 в порядке, но lemma4 выглядит странно для меня. AFAIK, и lemma3, и lemma4 не могут быть доказуемы одновременно. Я ожидал, что ключевое слово impossible в lemma4 не будет работать, и ожидал, что Idris покажет мне некоторые сообщения об ошибках о неправильном использовании impossible.
Является ли impossible небезопасным ключевым словом, которое можно использовать для подтверждения проверки типов?