haskell - 从 COQ 生成 Haskell 代码：使用的逻辑或参数值

Question

我目前正在尝试从我的程序验证引理生成 Haskell 代码，如下所示：

Lemma the_thing_is_ok : forall (e:Something),  Matches e (calculate_value e).

在结束我的部分后，我会：

Extraction Language Haskell.
Recursive Extraction the_thing_is_ok

它似乎对某事并不满意，因为它返回以下错误：

__ = Prelude.error "Logical or arity value used"

我有另一个引理，它似乎可以很好地导出，但我无法弄清楚问题到底出在哪里。有关如何解决该错误的任何线索？

Answer 1

CoqProp在提取过程中擦除类型的值——它们被认为没有计算意义。如果您的计算需要使用 a进行计算，Prop则提取将失败。