¿Qué significa V en la extensión de archivo Coq?

Question

¿Está .v para la verificación? ¿validación? vamanos?

¿Por qué no utilizar una extensión .coq?

Answer 1

Hay dos idiomas en Coq:

1. Gallina, el idioma plazo y
2. un idioma de administración llamado el Vernacular,

en particular:

Este el capítulo describe Gallina, el lenguaje de especificación de Coq. Permite desarrollar teorías matemáticas y pruebas de especificaciones de programas. Las teorías se construyen a partir de axiomas, hipótesis, parámetros, lemas, teoremas y definiciones de constantes, funciones, predicados y conjuntos. La sintaxis de los objetos lógicos involucrados en las teorías se describe en la Sección 1.2. El lenguaje de los comandos, llamado The Vernacular se describe en la sección 1.3.

Las extensiones de los archivos correspondientes son:

1. .g para los archivos de Gallina, que result from .v files después de eliminar las pruebas (véase también this message)
2. .v para archivos vernáculos.

Answer 2

En el reference manual lo llaman un "archivo vernacular".