2011-12-15から1日間の記事一覧
これはTheorem Proving Advent Calendarの15日目の記事である。 二回目じゃないのかって?人数不足だ。気にしてはいけない。 さて、今日の記事が何に関する記事かは見れば一目瞭然。 Coqの中のtactics記述用言語Ltacについてであり、目標はあの有名なcrushを…
これはTheorem Proving Advent Calendarの15日目の記事である。 二回目じゃないのかって?人数不足だ。気にしてはいけない。 さて、今日の記事が何に関する記事かは見れば一目瞭然。 Coqの中のtactics記述用言語Ltacについてであり、目標はあの有名なcrushを…