coqide - Trực tuyến trên đám mây

CHƯƠNG TRÌNH:

TÊN

coqide - Giao diện đồ họa Coq Proof Assistant

SYNOPSIS

coqide [ lựa chọn ]

MÔ TẢ

coqide là một giao diện đồ họa gtk cho trợ lý bằng chứng Coq.

Để sử dụng Coq theo hướng dòng lệnh, hãy xem coqtop(1); để sử dụng Coq theo hướng hàng loạt, hãy xem
coqc(1).

LỰA CHỌN

-h Hiển thị danh sách đầy đủ các tùy chọn được chấp nhận bởi coqide.

-I dir, bao gồm dir
Thêm dir thư mục trong đường dẫn bao gồm.

-R dir coqdir
Lập bản đồ đệ quy vật lý dir logic coqdir.

-src Thêm thư mục nguồn trong đường dẫn bao gồm.

-Là f, -trạng thái đầu vào f
Đọc trạng thái từ f.coq.

-ồn ào Bắt đầu với trạng thái trống.

-đầu ra f
Viết trạng thái trong tệp f.coq.

-load-ml-đối tượng f
Tải tệp đối tượng ML f.

-load-ml-nguồn f
Tải tệp ML f.

-l f, -load-vernac-nguồn f
Tải tệp Coq f.v (Tải f).

-lv f, -load-vernac-source-dài dòng f
Tải tệp Coq f.v (Tải chi tiết f).

-load-vernac-đối tượng f
Tải tệp đối tượng Coq f.vo.

-yêu cầu f
Tải tệp đối tượng Coq f.vo và nhập nó (Yêu cầu f).

-biên dịch f
Biên dịch tệp Coq f.v (ngụ ý -lô hàng).

-biên dịch-tiết f
Biên dịch chi tiết tệp Coq f.v (ngụ ý -lô hàng).

-opt Chạy phiên bản mã gốc của Coq hoặc Coq_SearchIsos.

-byte Chạy phiên bản bytecode của Coq hoặc Coq_SearchIsos.

-ở đâu In vị trí thư viện tiêu chuẩn của Coq và thoát.

-v In phiên bản Coq và thoát.

-q Bỏ qua việc tải rcfile.

-init-tệp f
Đặt rcfile thành f.

-lô hàng Chế độ hàng loạt (thoát ngay sau khi phân tích cú pháp đối số).

-khởi động Chế độ khởi động (ngụ ý -q và -lô hàng).

-emac Nói với Coq rằng nó được thực thi dưới Emacs.

-dump-cầu f
Kết xuất toàn cầu hóa trong tệp f (được sử dụng bởi coqdoc(1)).

-impredicative-bộ
Đặt sắp xếp Đặt ẩn ý.

-dont-chống tải
Không tải các bằng chứng không rõ ràng vào bộ nhớ.

-xml Xuất các tệp XML sang hệ thống phân cấp bắt nguồn từ thư mục
COQ_XML_LIBRARY_ROOT (nếu được đặt) hoặc thành stdout (nếu không được đặt).

Sử dụng coqide trực tuyến bằng các dịch vụ onworks.net