file - 在 Coq 文件扩展名中，V 代表什么？

Question

是.v为了验证吗？验证？瓦马诺斯？

为什么不使用.coq扩展程序？

Answer 1

Coq 中有两种语言：

1. Gallina，术语语言，和
2. 一种称为白话的管理语言，

尤其是：

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

对应的文件扩展名是：

1. .g对于 Gallina 文件，由删除校样后的.v文件产生（另请参阅此消息）
2. .v对于白话文件。

Answer 2

在参考手册中，他们称其为“白话文件”。