file - Coqファイル拡張子でVは何を表しますか？

Question

.v検証用ですか？検証？vamanos？

.coq拡張機能を使用してみませんか？

Answer 1

Coqには2つの言語があります。

1. ガリーナ、用語言語、および
2. 土語と呼ばれる管理言語、

特に：

この章では、Coqの仕様言語であるGallinaについて説明します。これにより、プログラムの数学的理論と仕様の証明を開発できます。理論は、公理、仮説、パラメーター、補題、定理、および定数、関数、述語、集合の定義から構築されます。理論に含まれる論理オブジェクトの構文については、セクション1.2で説明します。The Vernacularと呼ばれるコマンドの言語は、セクション1.3で説明されています。

対応するファイル拡張子は次のとおりです。

1. .g証明を削除した後のファイルから生じる.vGallinaファイルの場合（このメッセージも参照）
2. .v土語ファイルの場合。

Answer 2

リファレンスマニュアルでは、彼らはそれを「一般的なファイル」と呼んでいます。