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文件」。