証明駆動開発入門(2) 上記ページの勉強メモです。 Extraction coq から OCaml, Haskell, Scheme のコードを出力する。 OCaml にコードを出力するにはそのまま Extraction map. とすればいい。 これで (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **…

証明駆動開発入門(1) 何かを読む会 という社内勉強会が発足されました。 読んだ本の内容を共有しよう。 一人で勉強していてもダレるので共有することで無理やり進捗を出そう。 他の人の発表を聞いて読んだ気になろう。 っていう緩めの会です。 途中まで読ん…

お昼頃に予定があったので行くか迷っていたが、14時くらいには空いてきたということで技術書典2に行ってきた。 目当ての一つだったインターネットの闇さんのコンパイラの本は既に完売と向かってる最中の電車の中で知る。 Coqに興味があったのでCoqによる定理…

空のPathname同士をjoinした時に期待と違う挙動があった。 $ ruby -v ruby 2.3.3p222 (2016-11-21 revision 56859) [x86_64-darwin16] 期待していたのは次の動作。 path = Pathname.new('') # => #<Pathname:> path.join(path) # => #<Pathname:> でも実際はこうなっていた。 path </pathname:></pathname:>…