Revision 09cde0c1641959d197f88d2a31ca660406c41a83

Coq2Scala

#Coq to Scala

English

##概要 Coq2ScalaCoqのExtraction機能に関する拡張です。 Coq2ScalaはCoqで定義されたアルゴリズムをScalaと連携しJVM上で高速に動作させることを可能にします。

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

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

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

  1. あとはcoqと同様

##使い方

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

##coq2scalaを利用したソフトウェア - CoqInCoq for Scala

##未実装機能

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