- 2012-10-05 (Fri) 23:36
- 一般
Haskell と違って型以外の項もパラメータにとれるので色々と遊べる．自動でプログラムを変換させてみたりとか（基本となる関数の変換方法をインスタンスとして置いといて，それらの基本関数を適当に合成したものの変換結果を計算させるとか）．
とりあえず基本的なギミックは理解したので来週はもうちょい応用にチャレンジしよう．
閑話休題．
自明だけど証明が面倒（というか tactic の使い方に慣れてない）なので admit が大活躍してたりする今日この頃．慣れている人が証明してくれることを願いつつリポジトリに投げる．
- Newer: ことはじめ