4da: (Default)
Специалисты по 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)
Что-то буду писать под замком. А что-то - нет.
Добавляйтесь, кого не добавил.

September 2016

S M T W T F S
     123
45678910
11121314151617
18192021222324
252627282930 

Syndicate

RSS Atom

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 24th, 2017 06:33 pm
Powered by Dreamwidth Studios