4da: (Default)
[personal profile] 4da
Специалисты по 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


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

September 2016

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

Style Credit

Expand Cut Tags

No cut tags
Page generated Oct. 18th, 2017 02:07 am
Powered by Dreamwidth Studios