Co oznacza skrót V w rozszerzeniu pliku Coq?

Question

Czy weryfikacja jest przeprowadzana pod numerem .v? uprawomocnienie? vamanos?

Dlaczego nie używać rozszerzenia .coq?

Answer 1

w Coq Istnieją dwa języki:

1. Gallina, język termin i
2. językiem administracji nazywany Vernacular,

w szczególności:

ten rozdział opisuje Gallina, język specyfikacji Coq. Pozwala na opracowanie teorii matematycznych i dowodów specyfikacji programów. Teorie są zbudowane z aksjomatów, hipotez, parametrów, lematów, twierdzeń i definicji stałych, funkcji, predykatów i zbiorów. Składnia obiektów logicznych zaangażowanych w teorie została opisana w sekcji 1.2. Język poleceń, zwany Vernacular, opisany jest w rozdziale 1.3.

Odpowiednie rozszerzenia plików to:

1. .g plików Gallina, który result from .v files po usunięciu dowodów (patrz również this message)
2. .v plików języku narodowym.

Answer 2

W pliku reference manual nazywają go plikiem "vernacular".