.V 文件扩展名

供Coq使用的开发者文件。Coq是一款用于开发数学证明的应用程序；该文件以文本格式保存，包含使用Gallina语言编写的源代码。Gallina语言基于一种称为归纳构造演算（CIC）的表达力强的形式语言；V文件用于存储数学证明。

开发者使用Gallina“白话语法”在V文件中指定表达式。它是Gallina语言的命令语法，也就是命令语言。编写V文件后，你可以使用Coq证明助手IDE对其进行编译和运行，该程序名为CoqIDE。

注: Coq的开发工作此前由The Coq Development Team维护，现在由ADT Coq维护。ADT代表“技术发展行动”（Action for Technological Development）。

V文件包含使用V编程语言编写的源代码。通常，V文件包含V程序或模块。

你可以使用任何文本编辑器或源代码编辑器打开V文件并编辑其内容。源代码编辑器（例如Microsoft Visual Studio Code和GitHub Atom）包含一些实用工具，可以让你更轻松地阅读和编辑V文件。

如果你的V文件包含程序，你可以使用V的run命令运行该程序。

由基于Unix的程序ppmtoyuvsplit创建的原始“V”图像文件，该程序用于将Portable PixMap图像（.PPM文件）拆分为.Y、.U和V文件；存储图像的“V”色度（即颜色）分量；可以使用yuvsplittoppm工具将其还原为原始PPM文件。

V文件以Stanford MPEG编解码器所需的格式存储图像数据。

注: yuvsplittoppm和ppmtoyuvsplit命令行工具属于基于Unix的图形软件包netpbm。