en/Coq2Scala

#Coq to Scala

日本語

##Abstract

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

##Algorithm Mprime_annot

##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.

  1. Make and Install

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

##Examples - CoqInCoq for Scala: article

##Unsupported Features

  • Modules
  • CoInductive, CoFixpoint
  • Extract Inductive command