codice Generazione Haskell da COQ: Valore logico o arity utilizzato

Attualmente sto cercando di generare il codice Haskell dal mio programma di verifica lemma, che assomiglia a questo:codice Generazione Haskell da COQ: Valore logico o arity utilizzato

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

destro dopo aver terminato la mia sezione, lo faccio:

Extraction Language Haskell. 
Recursive Extraction the_thing_is_ok

E non sembra essere molto felice per qualcosa, dal momento che restituisce il seguente errore:

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

Ho un altro Lemma che sembra esportare bene ma non sono riuscito a capire quale fosse esattamente il problema. Eventuali indizi su come aggirare quell'errore?

fonte

2014-11-27 wtf8_decode

Il tuo Lemma è in Prop, come di solito è il caso? Credo che Coq scarti tutte le informazioni di Prop durante l'estrazione. Per esempio. se estrai '{n: nat | somePredicate n} 'otterrai un risultato naturale, ma senza la prova del predicato. – chi

Coq cancella i valori di tipo Prop durante l'estrazione: non vengono considerati significato computazionale. Se si dispone di un calcolo che richiede il calcolo con uno Prop, l'estrazione avrà esito negativo.

fonte

2014-11-27 18:29:03

Ok, capito! Qualche soluzione alternativa? –

Basta scrivere i tuoi oggetti di scena in Set. Tutto dovrebbe funzionare essenzialmente allo stesso modo, le uniche differenze funzionali sono esattamente ciò che rende l'interruzione dell'eliminazione del Prop. –

Super! Molte grazie ! –

codice Generazione Haskell da COQ: Valore logico o arity utilizzato

risposta

Problemi correlati