4da: (Default)
2016-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


Что там за год могло поменяться? 
4da: (Default)
2015-03-18 07:53 pm

Верхнепост

Что-то буду писать под замком. А что-то - нет.
Добавляйтесь, кого не добавил.