http://d.hatena.ne.jp/zyxwv/20070823 のモナド則から、Haskell でよく使われるモナド則を導く予定。これって Coq が使えるんじゃないだろうか。しっかり紙でやってしまったけども。 とりあえず簡単なやつから。導出できたら随時追記。 m * λa. unit a => m…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。