Есть ли способ извлечь абстракции, определенные в Coq, и связать их с кодом C ++?
Например, я хочу определить тип с именем EvenNum, который представляет все четные натуральные числа.Существуют ли какие-либо API / инструменты, которые я могу использовать на основе абстракции, которую я определил для этого нового типа - EvenNum, чтобы гарантировать, что сущности, которые я определил в C ++, не нарушают тип EvenNum?