Coq で練習してたファイルたちを github で管理。 rf0444's coq

9/18 に、GitとGitHubを体験しながら身につける勉強会に参加してきました。 USBメモリにぶち込んだ Ubuntu の初実践(?)。 merge とか使わない。rebase 使う。 (by bleis) .bashrc の PS1 に $(__git_ps) で現在のブランチを表示できる 自分の .bashrc もこん…

9/17 に、第11回名古屋Scala勉強会に参加してきました。 今回は23章と24章の予定だったけど、盛り上がったので24章は次回に。 23章 for 式の再説 モナド (1) bind : M[A] => (A => M[B]) => M[B] 最初の M[A] がレシーバ (Scala) return : A => M[A] この 2 …

Coqりさん 証明のかけら の続き (再挑戦)。 Require Import Arith. Fixpoint fib1 n:nat := match n with | 0 => 0 | 1 => 1 | S (S m as p) => fib1 p + fib1 m end. Fixpoint fib2 n a b:nat := match n with | 0 => a | S n => fib2 n b (a + b) end. Lem…

K I = F と、S K K = I を証明してみる。 Definition I {A:Type} x:A := x. Definition K {A B:Type} (x:A) (y:B) := x. Definition F {A B:Type} (x:A) (y:B) := y. Definition S {A B C:Type} (x:A->B->C) (y:A->B) (z:A) := x z (y z). Theorem ki_f : fo…

9/4 に、第1回 Scala座に行ってきました。 資料などはこちら。Ustream はこちら。 開会の挨拶 Scala座 全国レベルのScalaの勉強会！ 大きなイベントは関東が多い 悔しい！ → 名古屋で開催！ これまでのScala、これからのScala これまで編 Scalaって JVM上で…

F# の |> を Scala でやってみた。 scala> class Holder[A](a:A) { | def |>[B](f:A => B) = f(a) | } defined class Holder scala> implicit def any2holder[A](a:A) = new Holder(a) any2holder: [A](a: A)Holder[A] scala> val succ = (x:Int) => x + 1 s…

自分の Coq メモを晒してみる。 ■ ; について T1 ; T2 T1 適用後、T1 によって出来た全てのサブゴールに対して T2 を適用 T1 ; [T2 | T3] T1 適用後、T1 によって出来たサブゴール a, b に対して、a に T2、b に T3 を適用 (不要なら T2, T3 を省略可(何もし…