file - lectores - lector de archivos enc online

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

Question

Es .v para la verificación? ¿validación? vamanos?

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

Answer 1

En el manual de referencia lo llaman un "archivo vernacular ".

Answer 2

Hay dos idiomas en Coq:

1. Gallina , el término lenguaje, y
2. un lenguaje de administración llamado el Vernacular ,

en particular:

Este capítulo describe a 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 archivo correspondientes son:

1. .g para los archivos de Gallina, que resultan de los archivos .v después de eliminar las pruebas (vea también este mensaje )
2. .v para archivos vernaculares.