Agda trouble

Agda version 2.5.4.1 にあげたわけだけど、なんか、いくつか通らない証明が... 前にもそういうのあったんですが、

　　その時には、証明の方がおかしかった

引っかかったのは、monad から applicative を導くと言う奴で、Sets が絡んでいるので、いろいろ大変な奴... あらら。

赤が出ると type conflict なので完全に失敗してしまうわけなんですが、さすがに、そうはならないけど、

　　黄色くなる

これは、微妙なんですが、型の衝突はないが、

　　項が等しいと判断するのに十分に変数の値が代入されてない

みたいな感じらしいです。でも、証明は繋がってないのでダメ。だいたい、変数の対応を推論しきてれないことが多いので、
暗黙の変数({x}みたいな)を明示してやると通ることが多い。

多いわけですが、一度証明が通っているので、それほど簡単ではなく...

(λ r →

とか書いてるところを

(λ (r : ((b → c) → _ ) * (b → c) ) →

と書いたらなおったところが。う、うーん。

もう一ヶ所は、読みやすくするために、同値な項だけど形が違うものを書いていたりするんですが、

　　それを取り除いたら黄色が消えた

なるほど? 余計なことするなと。

最後のが苦労したんですが、

　　Product が builtin になったらしい

なんかλかなんかで定義されていたのに。それで、

　　normalized term の形がずれた

具体的には、項をまたがった Product の reduciton をやってくれなくなったみたい。変形して、そばに合わせてみたいな感じで逃げられました。

この手の微妙なのが Agda はなぁ。まぁ、学生が扱うにはそんなものは出てこないはずなんですけどね。

いやいや、今頃は、もっと他にやることあるだろ〜

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/rev/06388660995b