Generierung von Haskell-Code von COQ: Logisches oder arity Wert verwendet

Question

Ich bin derzeit versucht, Haskell Code von meinem Programmverifikation Lemma, die wie folgt aussieht zu generieren:

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

Gleich nach meinem Abschnitt endet, das tue ich:

Extraction Language Haskell. 
Recursive Extraction the_thing_is_ok 

Und es scheint nicht wirklich über etwas glücklich zu sein, da es die folgenden Fehler zurückgibt:

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

Ich habe ein anderes Lemma, das scheinbar gut exportiert, aber ich konnte nicht herausfinden, was das Problem genau war. Irgendwelche Hinweise, wie man diesen Fehler umgehen kann?

Answer 1

Coq löscht Werte des Typs Prop während der Extraktion - sie werden als keine Berechnungsbedeutung betrachtet. Wenn Sie eine Berechnung haben, die eine Berechnung mit einer Prop erfordert, wird die Extraktion fehlschlagen.