我正在尝试将 Coq 中使用Z数字的程序提取到 Haskell。我想将 Coq 的 Z 映射到 Haskell 的整数。
我找到了一些针对 OCaml 而不是针对 Haskell 的库。没有图书馆吗？
我需要提取物（在此处找到）：
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".
但瞄准Haskell。
我只想问：怎么办？
但其次，我应该说为什么我不能自己做：
我想我自己想不出这个可能是因为我误解了一些东西，例如：为什么第二个定义中有一个空字符串？的定义Z具有三个构造函数Z0：Zpos和Zneg。我看不出"Big.zero" "" "Big.opp"与此有什么关系。
另外，我不明白最后一个字符串是如何工作的：“......最后一个额外的字符串，指示如何在此归纳类型上执行模式匹配。” （在文档中找到）。
SF 的提取一章说“我们给出了一个 OCaml 表达式，它可以用作类型元素的‘递归’。（想想 Church 数字。）”。
下面的代码如何是递归或模式加工？
"(fun zero succ n →
if n=0 then zero () else succ (n-1))".
在我理解了这些事情之后，我希望我自己可以创造出我可能需要的提取物。