V что за файл?
Файл разработки, используемый Coq — приложением, применяемым для разработки математических проверок. Хранится в текстовом формате и содержит исходный код, который строится на языке Gallina, основывающемся на формальном языке, называемом Calculus of Inductive Constructions (CIC).
Разработчики определяют выражения в файлах V при помощи синтаксиса или языка команд Gallina «vernacular». После создания файлов V их можно компилировать и запускать в интегрированной среде разработки Coq Proof Assistant IDE – программе под названием CoqIDE.
Примечание: разработка Coq, управляемая прежде компанией The Coq Development Team, сейчас находится под руководством ADT Coq. ADT расшифровывается как «Action for Technological Development».
Чем открыть V
| CoqIDE |
| CoqIDE |
| CoqIDE |