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


Что там за год могло поменяться? 
From:
Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
User
Account name:
Password:
If you don't have an account you can create one now.
Subject:
HTML doesn't work in the subject.

Message:

 
Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.

September 2016

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

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 25th, 2017 06:03 am
Powered by Dreamwidth Studios