unsafePerformIOはよくわからん import System.IO.Unsafe main= do {c<-getChar; if (c ==':') then (putChar '\n') else (putChar c)>>main}のつもりで、 import System.IO.Unsafe main= let c = unsafePerformIO getChar in if (c ==':') then (putChar '\…

http://citeseer.ist.psu.edu/321720.html Buchbergerのアルゴリズム(Euclidのアルゴリズムが整数環のイデアルのよい生成元=最大公約数を求めるものであるのに対して、体係数の多項式環のイデアルのよい生成元=グレブナー基底を求めるアルゴリズム)をCoqで生…

ダメだーhttp://www.99-bottles-of-beer.net/ "99 Bottles of Beer"という歌を生成するという非常に簡単な問題を1000以上の言語で書いている。プログラム言語は数千あると一説には言われてるけどなかなか壮観。