EmptyCaseが入ってきた．absurd pattern matchingがHaskellで使えるのでHaskell証明士には朗報だ．具体的にEmptyCaseの有無で世界がどう変わるかを把握してる範囲で書く．まず，矛盾(bottom)の扱いについて．矛盾は「値を構成できない型」になればよいので，…

ghc-7.8でビルドできるAgdaマダカナーとか思いつつ，Agda-2.3.4のリリースノート(まだリリースされてないけど)を眺めてたら，実験的機能としてcopatternsってやつが入ると書かれている．余(co-)がついてるのでたぶん健康によくないやつなんだろうなと思いつ…

ghc-mod-4以降ではghc-modiを使うためにflymakeへの依存を切っており，flymake的な挙動は自前で実現している．そのため，今まで反映されていたflymake用のface設定が反映されなくなるので，バージョンアップ後急にさびしい絵面になったりする．もし， (set-f…