4da: (Default)
4da ([personal profile] 4da) wrote2016-09-01 02:10 am
Entry tags:

Проблемы с totality checker в Idris 0.12.2

Специалисты по idris есть?
Объясните почему Algebraic.idr из lambdaconf 2015 не тайпчекается свежим идрисом?

Конкретно вот на этом участке
notNotIdempotent : (b : Bool) -> Idempotent not b -> Void
notNotIdempotent False Refl impossible
notNotIdempotent True Refl impossible


Вываливает ошибку:
- + Errors (1)
 `-- algebraic.idr line 40 col 17:
     notNotIdempotent False Refl is a valid case


Что там за год могло поменяться?