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

Question

是否使用.v进行验证？验证？ vamanos？

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

Answer 1

Coq中有两种语言:

Gallina，术语语言和

一种称为Vernacular的管理语言，

特别是:

This chapter describes Gallina, the specification language of Coq. It allows developing mathematical theories and proofs of specifications of programs. The theories are built from axioms, hypotheses, parameters, lemmas, theorems and definitions of constants, functions, predicates and sets. The syntax of logical objects involved in theories is described in Section 1.2. The language of commands, called The Vernacular is described in section 1.3.

相应的文件扩展名是:

galat文件的

.g，在删除证明后为result from .v files(另请参见this message)

本地文件的

.v。