Controllo dell'esportazione di costruttori nel codice estratto da Coq

Question

Sto guardando il codice di scrittura in Coq ed estraendo questo codice per l'utilizzo in un grande progetto Haskell. Voglio costruire un singolo modulo in Coq, provare le proprietà, quindi utilizzare il sistema dei moduli di Haskell per prevenire la violazione di queste proprietà (tramite costruttori intelligenti).

Non riesco a trovare alcuna indicazione che sia possibile estrarre il codice Coq in un modulo Haskell con un elenco di esportazione esplicito. Sembra che devo modificare a mano il codice Coq estratto, che non è un grosso problema, ma voglio sapere se ho questo diritto. Qualcuno ha una proposta alternativa?

Answer 1

Ho appena guardato l'ultimo coq source (r14456). Non sembra esserci alcun codice per generare una lista di esportazione.

Sembra che dovrai farlo tu stesso.