2009-04-24から1日間の記事一覧
(12/12更新) eq型のパターンマッチを使って型を書き換えるテクニックを 知ったので、mcomposeの書き直し。 型がMorphism A B -> Morphism B C -> Morphism A Cで、計算できるものができた。 ただし諸定理の定義をDefined.でTransparentにしておかないとうま…
(12/12更新) eq型のパターンマッチを使って型を書き換えるテクニックを 知ったので、mcomposeの書き直し。 型がMorphism A B -> Morphism B C -> Morphism A Cで、計算できるものができた。 ただし諸定理の定義をDefined.でTransparentにしておかないとうま…