coq-extraction

1熱度

1回答

嗨我寫的勒柯克到ocaml的提取，我想轉換類型： positive --> int32 N -> int32 ，但我想保持類型Z是int 這是我做的提取這些代碼條件： Require Import ZArith NArith. Require Import ExtrOcamlBasic. (* Mapping of [positive], [N], [Z] into [int32].

2熱度

1回答

COQ類型的NAT萃取到哪種類型的ocaml的，這樣我可以有一個已驗證的程序

在Coq，從nat類型提取到int或big_int未經認證（他們是有效的）。正如下面這些鏈接： http://coq.inria.fr/V8.3/stdlib/Coq.extraction.ExtrOcamlNatBigInt.html 和 http://coq.inria.fr/distrib/8.3/stdlib/Coq.extraction.ExtrOcamlNatInt.html 兩個說：

1熱度

1回答

OCaml的串和串Coq的（提取Coq的至OCaml的）

3熱度

1回答

從Coq提取生成後使用函數Ocaml

我有一個文件夾tmp這是我從coq提取到ocaml後生成的。 ~/tmp/cpf0.ml cpf0.mli cpf0.o cpf0.cmi cpf0.cmx cpf0.cmo main.ml是我用來調用一個函數cpf0文件： let prf = Cpf0.proof;; 我得到了一個錯誤說Cpf0.proof綁定。我試過用：（proof存在於Cpf0）。 open Cpf0;; let

0熱度

1回答

Coq生成「failwith」AXIOM將被實現的提取機制「」

我在這個模塊裏面有一個模塊結構我在module A裏聲明瞭一些函數的變量用法。 Module A. Variable a : nat. End A. 然後我使用提取機制。 Extraction Language Ocaml. Set Extraction Optimize. Set Extraction AccessOpaque. Extraction A. 或只是

7熱度

1回答

如何在將Coq提取到Haskell時設置模塊名稱

當我使用Coq文件中的Extraction Language Haskell.將Coq提取/編譯成Haskell並運行coqtop -compile mymodule.v > MyModule.hs時，我得到一個以module Main where開頭的Haskell模塊。是否有選項可以設置生成的Haskell模塊名稱？我現在管的sed這樣的 - coqtop -compile mymodul

4熱度

2回答

string_dec和串

我有文件： String0.ml從String.v（它是從Coq的庫） String.ml萃取：是ocaml的的字符串庫將我的測試文件從Coq提取到Ocaml後，我想在Ocaml的庫中使用String.ml，所以我編寫了一個替換com將所有String0替換爲String。的問題是文件test.v中，我使用的定義之一： Definition beq_string := beq_dec str

2熱度

1回答

轉換NAT在勒柯克提取big_int到Ocaml程序編寫

我做提取轉換nat到big_int 當我使用的庫：ExtrOcamlNatBigInt，它不big_int在Ocaml 所以我返回正確的類型修改它（文件ExtrOcamlNatBigInt），但我找不到定義函數nat_case的方式，因爲在Ocaml的庫文件Big_int中它們沒有函數nat_case。 Extract Inductive nat => "Big_int.big_int"

0熱度

1回答

通過在Coq中使用「遞歸提取」提取到OCaml文件

我想將Coq中的函數foo提取爲OCaml文件。因爲我的真實功能必須使用Recursive Extraction，所以當我運行一個程序時，它會在cmd上輸出提取的OCaml代碼。但我想它輸出到文件，例如：foo.ml Recursive Extraction foo. 當我想： Recursive Extraction "foo.ml" foo. 或Recursive Extraction