en/Coq2Scala

#Coq to Scala

日本語

##Abstract

Coq2Scala is an extention to Coq Extraction. Coq will be able to generate Scala code from Coq definitions.

• author: Yoshihiro Imai(IT Planning Inc), Jiang Fan(The University of Tokyo)
• hashtag: #coq2scala
• sources: http://bitbucket.org/yoshihiro503/coq2scala

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

https://bitbucket.org/yoshihiro503/coq2scala/downloads

##Install 1. Download the patch file and corresponding version of Coq source code from CoqDistributes. 2. Apply the patch.

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

3. Make and Install

   $ ./configure -prefix ~/coq2scala
   $ make world
   $ make install

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

##Examples - CoqInCoq for Scala

##Unsupported Features

• Modules
• CoInductive, CoFixpoint
• Extract Inductive command