从COQ生成Haskell代码:使用逻辑或arity值

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"

我有另一个Lemma似乎确实输出得很好,但我无法弄清楚究竟是什么问题.有关如何解决该错误的任何线索？

Answer 1

Coq Prop在提取期间删除类型的值- 它们被认为没有计算意义.如果你有一个需要计算的计算,Prop那么提取就会失败.