Что означает V в расширении файла Coq?

Question

.v для проверки? Проверка? vamanos

Почему бы не использовать расширение .coq?

Answer 1

В Coq есть два языка:

1. Галлина , термин язык и
2. административный язык, называемый народный ,

, в частности:

Эта глава описывает Gallina, язык спецификации Coq. Это позволяет разрабатывать математические теории и доказательства спецификаций программ. Теории построены из аксиом, гипотез, параметров, лемм, теорем и определений констант, функций, предикатов и множеств. Синтаксис логических объектов, задействованных в теориях, описан в разделе 1.2. Язык команд, называемый Vernacular, описан в разделе 1.3.

Соответствующие расширения файлов:

1. .g для файлов Gallina, которые получаются из .v файлов после удаления доказательств (см. Также это сообщение )
2. .v для обычных файлов.

Answer 2

В справочном руководстве они называют его " народным файлом".