Конвертировать nat в big_int для извлечения Coq в Ocaml

Question

Я делаю извлечение конвертировать nat в big_int

Когда я использовал библиотеку: ExtrOcamlNatBigInt, она не возвращает правильный тип для big_int в Ocaml

Поэтому я изменяю его (файл ExtrOcamlNatBigInt), но не могу найти способ определить функцию nat_case потому что в библиотеке Big_int Ocaml у них нет функции nat_case,

Extract Inductive nat => "Big_int.big_int"
  [ "Big_int.zero_big_int" "Big_int.succ_big_int" ] "Big_int.nat_case".

Я пытаюсь определить второе определение nat_case от:

Extract Inductive nat => "Big_int.big_int"
  [ "Big_int.zero_big_int" "Big_int.succ_big_int" ] "(fun fO fS n ->
    let one = Big_int.unit_big_int in
    if n = Big_int.zero_big_int then fO () else fS (n - one))".

Вот результат после использования второго определения:

(** val nat_rect :
    'a1 -> (Big_int.big_int -> 'a1 -> 'a1) -> Big_int.big_int -> 'a1 **)

let rec nat_rect f f0 n =
  let one = Big_int.unit_big_int in
    if n = Big_int.zero_big_int then f () else f0 (n - one)
    (fun _ ->
    f)
    (fun n0 ->
    f0 n0 (nat_rect f f0 n0)) n

Я получил ошибку в n линии else f0 (n - one):

Файл "Datatypes.ml", строка 68, символы 51-52: Ошибка: это выражение имеет тип Big_int.big_int, но ожидалось выражение типа int

Я думаю, что это из-за minus (-)

Я также изменяю minus добыча:

Extract Constant minus => "fun n m -> Big_int.max_big_int Big_int.zero_big_int 
   (Big_int.sub_big_int n m)".

Не могли бы вы помочь мне определить функцию nat_case за Big_int? Большое спасибо.

Answer 1

(-) зарезервировано для целочисленной операции, вы не можете использовать тот же оператор для big_int, замещать

(n - one)

от:

Big_int.sub_big_int n one