はじめに この記事はF# Advent Calendar 2014の10日目の記事です。 前日はbleisさんの「クラスのコンストラクタ呼び出し時にプロパティも同時に初期化する」でした。 本日はTipsからちょっと外れてネタをご紹介します。 タイトルにもある通り、コンピュテー…

久々の記事もまたCoqでソフトウェアの基礎ネタです。 今回はList_Jにおける練習問題「rev_injective」について。 問題のTheorem Theorem rev_injective: forall l1 l2: natlist, rev l1 = rev l2 -> l1 = l2. ソフトウェアの基礎ではCoqコードではありません…

はい、表題のとおりです。 Coqを勉強していたらよくわからない挙動にぶつかったのでメモ。 問題のコード Fixpoint evenb (n:nat) : bool := match n with | O => true | S O => false | S (S n') => evenb n' end. Definition oddb (n:nat) : bool := negb (…

ちょっとした前置き TaPL？ TAPL？ どっちなんでしょう。 ということで8月2日に開催されたTAPL読書会@名古屋#1に参加しました。 短歌会館というところの和室を借りて行いました。非常に雰囲気の良い所でしたので、お勧めです。 ただし無線LANとかはないので…