coq2scalaをさわってみた
http://proofcafe.org/wiki/Coq2Scala を試してみました。 インストールはhgでソースコードとってきて、 ./configure make world make install でおｋ。 Extraction Language Scala. が使えちゃうCoqがインストールされます。 使ってみた とりあえず自然数と足し算を定義してみます。 吐き出されたScalaのコード。 Notationは無視される？ パラメータとらない場合はcase object使って欲しいかも・・・・ あとインデントも付くとうれしい。 ClassとInstanceを使ってみる Monoidを定義してみた。 私はtraitとimplicit parameterでかっこ良く変換されるのかな！？と期待。 結果は・・・・・ (´・ω・｀)ｼｮﾎﾞｰﾝ 明示的にインスタンスを渡して関数を得る感じ
Coqはじめました。
あけましておめでとうございます。 何か新しいことをはじめようと思い、Coqに手を出しました。 まだ慣れていないけど、なかなか楽しいです。 証明楽しいとかどんな変態（褒め言葉）なんだ！ と思っていましたが、私も無事変態の仲間に入ることが出来ました。 Coqをはじめる Coqを使い始めたきっかけは冬休みの宿題で読書感想文です。 私は選んだ本はもちろん「数学ガール」。 なかなかおもしろいのでオススメです。 数学が得意というわけでもない私は、理解の手助けとしてプログラムを書こうと思いました。 そこでCoqの登場です！ 本に出てくる命題を証明していくことにしました。 Coqに関する資料は決して多くありませんが、良いチュートリアルがあるので、まずはこれらを参考にしましょう。 http://www.iij-ii.co.jp/lab/techdoc/coqt/ http://www.slideshare.
ポジティブ型とマイポジティブ型 - にわとり小屋でのプログラミング
（＊＊ Remark 今回はZArithモジュールを使うよ。 Require Import ZArith. をタイプしてね。 ＊） 導入 Coqでは、整数全体の型はZで表され、次のように定義されている。 Coq < Print Z. Inductive Z : Set := Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z Z0はゼロで、Zposは正の数、Znegは負の数を表している。 ここでpositiveという型が使われているが、これは１以上の整数全体を表している。 Coqでは、このpositive型に工夫がしてあって、現実のプログラムとの親和性をよくしている。 具体的には次のような再帰的な定義になっている。 Coq < Print positive. Inductive positive : Set := xI : positi
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
