Haskell code generation from COQ: using boolean value or arity value

Question

I'm currently trying to create Haskell code from my program verification lemma, which looks like this:

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

Immediately after the end of my section, I:

 Extraction Language Haskell. Recursive Extraction the_thing_is_ok 

And this, it seems, is not very happy, because it returns the following error:

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

I have one more lemma that seems to be exporting just fine, but I couldn't figure out what the problem is. Any clues on how to get around this error?

Answer 1

Coq erases values ​​of type Prop during extraction - they are considered to have no computational meaning. If you have a computation that requires computation with Prop , then the extraction will fail.