V代表Coq文件扩展名是什么意思？

Question

是否为.v进行验证？验证？ vamanos？

为什么不使用.coq的扩展？

Answer 1

有两种语言在勒柯克：

1. Gallina，术语的语言，并
2. 称为Vernacular的管理语言，

特别是：

这章节描述了Gallina，Coq的规范语言。它允许开发程序规范的数学理论和证明。理论是建立在公理，假设，参数，引理，定理和常数，函数，谓词和集合的定义之上的。 1.2节描述了涉及理论的逻辑对象的语法。命令的语言，称为The Vernacular在1.3节中描述。

相应的文件扩展名是：

1. .g为加利纳文件，这result from .v files除去样张后（也见this message）
2. .v为乡土文件。

Answer 2

在reference manual中，他们称之为“vernacular文件”。