Đây là coqc lệnh có thể chạy trong nhà cung cấp dịch vụ lưu trữ miễn phí OnWorks bằng cách sử dụng một trong nhiều máy trạm trực tuyến miễn phí của chúng tôi như Ubuntu Online, Fedora Online, trình giả lập trực tuyến Windows hoặc trình giả lập trực tuyến MAC OS
CHƯƠNG TRÌNH:
TÊN
coqc - Trình biên dịch Coq Proof Assistant
SYNOPSIS
coqc [ chung Gà trống lựa chọn ] hồ sơ
MÔ TẢ
coqc là trình biên dịch hàng loạt cho Coq Proof Assistant. Các tùy chọn về cơ bản là
giống như coqtop(1). tập tin.v là tệp bản địa để biên dịch. hồ sơ chỉ phải được hình thành
với các ký tự `a` đến` Z`, `0`-`9` hoặc` _` và phải bắt đầu bằng một chữ cái. Các
trình biên dịch tạo ra một tệp đối tượng tập tin.vo.
Để sử dụng tương tác Coq, hãy xem coqtop(1).
LỰA CHỌN
coqc là một tập lệnh chỉ đơn giản chạy coqtop với tùy chọn -biên dịch nó chấp nhận các tùy chọn tương tự
as coqtop.
-hình ảnh bin
sử dụng bin như cơ bản coqtop thay vì mặc định.
-bèo thuyền
in tệp đã biên dịch trên đầu ra chuẩn.
Sử dụng coqc trực tuyến bằng các dịch vụ onworks.net