Che cosa significa V sta per nell'estensione di file Coq?

Question

È .v per la verifica? convalida? vamanos?

Perché non utilizzare l'estensione .coq?

Answer 1

Ci sono due lingue in Coq:

1. Gallina, il linguaggio termine, e
2. un linguaggio di amministrazione chiamato Vernacular,

in particolare:

Questo capitolo descrive Gallina, il linguaggio delle specifiche di Coq. Permette lo sviluppo di teorie matematiche e prove delle specifiche dei programmi. Le teorie sono costruite da assiomi, ipotesi, parametri, lemmi, teoremi e definizioni di costanti, funzioni, predicati e insiemi. La sintassi degli oggetti logici coinvolti nelle teorie è descritta nella Sezione 1.2. Il linguaggio dei comandi, chiamato The Vernacular è descritto nella sezione 1.3.

Le estensioni dei file corrispondenti sono:

1. .g per i file Gallina, che result from .v files dopo aver rimosso le prove (vedi anche this message)
2. .v per i file volgare.

Answer 2

Nel reference manual lo chiamano "file vernacular".