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

[4da]

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

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

Вываливает ошибку:
- + Errors (1

Comments

[zeit_raffer]

Создайте issue им на гитхабе. Я раньше так делал. Там всегда отаечают.

[zeit_raffer]

Ага! Идентификаторы с малееькой буквы считаются теперь переменными. Там not надо переименовать, чтобы была с большой буквы. И остальные функции тоже.

спасибо

[4da]

Ну, Not это функция из типа в тип:
λΠ> :t Not
Not : Type -> Type

Код тайпчекается если заменить not на Bool.not