#Coq to Scala

[English](/en/Coq2Scala)

##概要
[Coq2Scala]()は[Coq](http://coq.inria.fr/)のExtraction機能に関する拡張です。
Coq2ScalaはCoqで定義されたアルゴリズムを[Scala](http://scala-lang.org/)と連携しJVM上で高速に動作させることを可能にします。

- 開発者: [@yoshihiro503](http://twitter.com/yoshihiro503)
- ハッシュタグ: [#coq2scala](https://twitter.com/#!/search/realtime/%23coq2scala)
- リポジトリ: [http://bitbucket.org/yoshihiro503/coq2scala](http://bitbucket.org/yoshihiro503/coq2scala)

##ダウンロード
こちらから差分をダウンロードできます:

[https://bitbucket.org/yoshihiro503/coq2scala/downloads](https://bitbucket.org/yoshihiro503/coq2scala/downloads)

##インストール
1. 上記から差分ファイルをダウンロードし、対応するcoqのソースコードも[Coq本家](http://coq.inria.fr/distrib/)から取得します。
2. patchコマンドでパッチを適用します。

~~~ { .sh }
   $ cd coq-8.3pl2/
   $ patch -p 2 < ~/Downloads/coq2scala-1.0_for_coq-8.3pl2
~~~

3. あとはcoqと同様

~~~ { .sh }
   $ ./configure -prefix ~/coq2scala
   $ make world
   $ make install
~~~

##使い方

Extraction Language Scala. と指定し、あとは通常のCoqと同様。

##coq2scalaを利用したソフトウェア
- [CoqInCoq for Scala](http://d.hatena.ne.jp/yoshihiro503/20111207#p1)

##未実装機能

- モジュール機能
- CoInductive, CoFixpoint
- Extract Inductiveコマンドによる指定