Sterowanie eksportowaniem konstruktorów w kodzie wyekstrahowanym z Coq

Question

Czekam na pisanie kodu w Coq i wyodrębnianie tego kodu do użycia w dużym projekcie Haskell. Chcę zbudować pojedynczy moduł w Coq, udowodnić właściwości, a następnie użyć systemu modułowego Haskell, aby zapobiec naruszeniu tych właściwości (za pośrednictwem inteligentnych konstruktorów).

Nie mogę znaleźć żadnego wskazania, że ​​możliwe jest wyodrębnienie kodu Coq do modułu Haskell z jawną listą eksportową. Wydaje się, że muszę ręcznie zmodyfikować wyodrębniony kod Coq, co nie jest wielką sprawą, ale chcę wiedzieć, czy mam to prawo. Czy ktoś ma alternatywną propozycję?

Answer 1

Właśnie patrzyłem na najnowsze źródło coq (r14456). Wydaje się, że nie istnieje żaden kod do generowania listy eksportu.

Wygląda na to, że musisz to zrobić sam.