#Coq to Scala

[日本語](/wiki/Coq2Scala)

##Abstract

[Coq2Scala]() is an extention to [Coq](http://coq.inria.fr/) Extraction.
Coq will be able to generate Scala code from Coq definitions.

- author: [@yoshihiro503](http://twitter.com/yoshihiro503)
- hashtag: [#coq2scala](http://twitter.com/#!/search?q=%23coq2scala)
- sources: [http://bitbucket.org/yoshihiro503/coq2scala](http://bitbucket.org/yoshihiro503/coq2scala)

##Download
The extension is provided as a patch for Coq source code:

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

##Install
1. Download the patch file and corresponding version of Coq source code from [CoqDistributes](http://coq.inria.fr/distrib/).
2. Apply the patch.

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

3. Make and Install

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

##How to Use
The vernacular command : "Extraction Language Scala." will be available.

##Examples
- [CoqInCoq for Scala](http://d.hatena.ne.jp/yoshihiro503/20111207#p1)

##Unsupported Features

- Modules
- CoInductive, CoFixpoint
- Extract Inductive command