前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。 動機 let多相の実装はしたから、次は証明だろ 最近、流行っているCoqを覚えたい 扱えるラムダ式 型は、Bool型と関数型のみ。 Inductive type : Set := | BoolT …

30分プログラム、その699。いつ、どこで、誰が、何をしたジェネレータ。 ランダムに文章を生成するよ! Printfがとっても欲しいよ! 使い方 昨日、海でキミが寝たval it = () : unit - println (make ()); 昨日、地の中で知らない人が食事をした val it = () :…