型によるしりとりの成立判定 - コンピュータってすごいらしい(12/12更新) eq型のパターンマッチを使って型を書き換えるテクニックを 知ったので、mcomposeの書き直し。 型がMorphism A B -> Morphism B C -> Morphism A Cで、計算できるものができた。 ただし諸定理の定義をDefined.でTransparentにしておかないとうまくいかない模様。 概要 依存型プログラミング(Coq)の練習のために モニャドセミナー第1回 http://d.hatena.ne.jp/m-hiyama/20090414/1239686984 で知ったしりとりの圏 http://d.hatena.ne.jp/m-hiyama/20090424/1240552575 を実装しようと試みている。 (4/25少し更新。) 依存型と圏の射 Coqを知らない人に見てほしいことは mkobuta(Morphismとしてのこぶた)が"
