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

Question

我在這個模塊裏面有一個模塊結構我在module A裏聲明瞭一些函數的變量用法。

Module A. 

    Variable a : nat. 

End A. 

然後我使用提取機制。

Extraction Language Ocaml. 
Set Extraction Optimize. 
Set Extraction AccessOpaque. 
Extraction A. 

或只是

Extraction A. 

它產生了我一個警告的代碼： 「下面的公理必須在提取的代碼實現：AA」

type nat = 
| O 
| S of nat 

module A = 
struct 
    (** val a : nat **) 

    let a = 
    failwith "AXIOM TO BE REALIZED" 
end 

這裏我收到a與failwith "AXIOM TO BE REALIZED" 我無法運行我的功能成功因爲此failwith

因爲我必須在模塊內部使用變量a。 我想知道有沒有一種方法來定義一個模塊，它將不會在提取後生成failwith？或者與抽取相關的東西不會生成failwith函數？

Answer 1

那麼，在某些時候，您將不得不提供A.a的值。如果你想抽象A相對於a，我想這是最簡便的方法是使用仿函數，它直接OCaml中翻譯成這樣：

Module Type Param. 
    Variable x: nat. 
End Param. 

Module A (Import P: Param). 

    Definition a:=P.x. 

End A. 

Extraction Language Ocaml. 
Set Extraction Optimize. 
Set Extraction AccessOpaque. 

Extraction "test.ml" A. 

（當然，你必須實例化導致的OCaml函數A來運行計算）。