Я смотрю на написание кода на Coq и на извлечение этого кода для использования в большом проекте на Haskell.Я хочу построить один модуль в Coq, доказать свойства, а затем использовать систему модулей Haskell, чтобы предотвратить нарушение этих свойств (с помощью умных конструкторов).
Я не могу найти никаких признаков того, что можно извлечь код Coqв модуль Haskell с явным списком экспорта.Кажется, я должен вручную изменить извлеченный код Coq, что не имеет большого значения, но я хочу знать, имею ли я это право.У кого-нибудь есть альтернативное предложение?