Как извлечь Coq's Z в целое число Хаскелла

Question

Я пытаюсь извлечь в Haskell программу на Coq, которая использует Z номера. Я хочу отобразить Coq's Z на целое число Хаскелла.

Я нашел несколько библиотек для этой цели, но не для Хаскелла. Для этого нет библиотеки?

Мне нужны извлечения (найдены здесь):

Extract Inductive positive => "Big.big_int"
 [ "Big.doubleplusone" "Big.double" "Big.one" ] "Big.positive_case".

Extract Inductive Z => "Big.big_int"
 [ "Big.zero" "" "Big.opp" ] "Big.z_case".

Extract Inductive N => "Big.big_int"
 [ "Big.zero" "" ] "Big.n_case".

но целится в Хаскелл.

Я просто спрошу: как это сделать?

Но во-вторых, я должен сказать, почему я не мог сделать это сам:

Наверное, я не могу придумать это сам, возможно, потому что я неправильно понимаю кое-что, например: почему во втором определении есть пустая строка? Определение Z имеет три конструктора: Z0, Zpos а также Zneg, Я не вижу как "Big.zero" "" "Big.opp" связано с этим.

Кроме того, я не понял, как работает последняя строка: "... последняя дополнительная строка, которая указывает, как выполнить сопоставление с образцом для этого индуктивного типа". (найдено в документации).

В главе " Извлечение SF" говорится, что "мы даем выражение OCaml, которое можно использовать в качестве" рекурсора "для элементов типа. (Подумайте о церковных цифрах.)".

Как приведенный ниже код является рекурсором или выполняет паттерны?

  "(fun zero succ n →
      if n=0 then zero () else succ (n-1))".

После того, как я пойму эти вещи, я надеюсь, что смогу сам извлечь извлечения, которые мне могут понадобиться.

Answer 1

Вы можете просто импортировать ExtrHaskellZInteger ( документация).