Механизм извлечения Coq генерирует "failwith "AXIOM TO REALIZE""

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 запустить вычисления).