Generating Haskell code from COQ: Logical or arity value used

Question

I am currently trying to generate Haskell code from my program verification lemma, which looks like this:

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

Right after ending my Section, I do:

Extraction Language Haskell.
Recursive Extraction the_thing_is_ok

And it does not seem to be really happy about something, since it returns the following error:

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

I have another Lemma which does seem to export just fine but I could not figure out what the problem was exactly. Any clues on how to work around that error?

Answer 1

Coq erases values of type Prop during extraction—they're considered to have no computational meaning. If you have a computation which requires computing with a Prop then extraction will fail.