何となく自分で何がしたかったのか思い出したのと、色々混乱してたのと。例えば、私としては、HaskellやCleanのような言語でtupleが圏論的な意味での積になってることを示したい。tupleが圏論的な意味で積になってるというのは、任意の型a,b,cと関数f:c->a,g…

さて、Sparkleでsortの正しさを証明しようと思った。めんどいので、isSortedという関数を用意して、"isSorted (sort ls)=True"を証明しようとしたのだけど、オーバーローディングが解決できません！とか怒られる(なお自前の関数を利用するには、.iclファイル…

Coqとかに比べて、Sparkleユーザって、世界に10人くらいしかいなそうなので(いや知らんけどね)、なんかもうナンバー1よりオンリー1って感じだよな〜(何が一応マニュアルっぽいものはあった。マニュアルというには、アレだが http://www.cs.kun.nl/~marko/res…

とりあえず、使ってみないと分からんよな〜という話なんだが、Sparkleってマニュアルとかないのかよ。Cleanコミュニティのやる気のなさは異常(まあ単に人が少ないというだけなんだろうが)。細かくメモっとかないと自分で使い方を忘れそうlol 0.Sparkleが組み…