Генерация кода на Haskell из COQ: используется логическое значение или значение арности

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

Coq стирает значения типа Prop во время извлечения - они не имеют вычислительного значения. Если у вас есть вычисления, которые требуют вычисления с Prop тогда извлечение не удастся.