V đứng trong phần mở rộng của tệp Coq là gì?

Question

Có phải là .v để xác minh không? xác nhận? vamanos?

Tại sao không sử dụng tiện ích mở rộng .coq?

Answer 1

Có hai ngôn ngữ trong Coq:

1. Gallina, ngôn ngữ hạn, và
2. một ngôn ngữ chính được gọi là Vernacular,

đặc biệt:

này chương mô tả Gallina, ngôn ngữ đặc tả của Coq. Nó cho phép phát triển các lý thuyết toán học và bằng chứng về thông số kỹ thuật của chương trình. Các lý thuyết được xây dựng từ tiên đề, giả thuyết, tham số, bổ đề, định lý và định nghĩa của hằng số, hàm, vị từ và tập hợp. Cú pháp của các đối tượng logic liên quan đến các lý thuyết được mô tả trong Phần 1.2. Ngôn ngữ của các lệnh, được gọi là The Vernacular được mô tả trong phần 1.3.

Các phần mở rộng tập tin tương ứng là:

1. .g cho các tập tin Gallina, mà result from .v files sau khi loại bỏ các bằng chứng (xem thêm this message)
2. .v cho các tập tin bản xứ.

Answer 2

Trong số reference manual, chúng gọi đó là tệp "vernacular".