Coq에서 추출한 코드에서 생성자의 내보내기 제어하기

Question

저는 Coq에서 코드를 작성하고이 코드를 추출하여 대형 하스켈 프로젝트에서 사용하려고합니다. Coq에서 하나의 모듈을 만들고 속성을 증명 한 다음 Haskell의 모듈 시스템을 사용하여 스마트 생성자를 통해 이러한 속성의 위반을 방지합니다.

명백한 내보내기 목록이있는 Haskell 모듈에 Coq 코드를 추출 할 수 있다는 어떠한 징후도 발견 할 수 없습니다. 추출한 Coq 코드를 직접 수정해야하는 것 같습니다. 큰 문제는 아니지만이 권리가 있는지 알고 싶습니다. 대체 제안이있는 사람이 있습니까?

Answer 1

방금 ​​최신 coq 소스 (r14456)를 살펴 보았습니다. 내보내기 목록을 생성하는 코드가없는 것 같습니다.

직접 해봐야 할 것 같습니다.