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

CHƯƠNG TRÌNH:

TÊN

coqtop - Hệ thống cấp trên cùng của Coq Proof Assistant

SYNOPSIS

coqtop [ lựa chọn ]

MÔ TẢ

coqtop là hệ thống cấp cao nhất của Coq, để sử dụng tương tác. Nó đọc các cụm từ trên
đầu vào tiêu chuẩn và in kết quả trên đầu ra tiêu chuẩn.

Để sử dụng Coq theo hướng hàng loạt, hãy xem coqc(1).

LỰA CHỌN

-NS, --Cứu giúp
Cứu giúp. Sẽ cung cấp cho bạn danh sách đầy đủ các tùy chọn được coqtop chấp nhận.

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

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

-hàng đầu coqdir
đặt tên cấp cao nhất là coqdir thay vì Top

-trạng thái đầu vào tên tệp, -Là tên tập tin
đọc trạng thái từ tệp tên tệp.coq

-ồn ào bắt đầu với trạng thái ban đầu trống rỗng

-đầu ratên tập tin
ghi trạng thái trong tệp tên tệp.coq

-load-ml-đối tượng tên tập tin
tải tệp đối tượng ML tên tập tin

-load-ml-nguồn tên tập tin
tải tệp ML tên tập tin

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

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

-load-vernac-đối tượng tên tập tin
tải tệp đối tượng Coq tên tệp.vo

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

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

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

-opt chạy phiên bản mã gốc của Coq

-byte chạy phiên bản bytecode của Coq

-ở đâ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 tải rcfile

-init-tệp tên tập tin
đặt rcfile thành tên tập tin

-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 tên tập tin
kết xuất toàn cầu hóa trong tệp f (được sử dụng bởi coqdoc(1) )

-với-không thấm nước (có | không)
để (de) kích hoạt các chức năng đặc biệt cho Geoproof trong Coqide (mặc định là Vâng )

-impredicative-bộ
thiết lập sắp xếp Đặt ẩn ý

-dont-chống tải
không tải các bằng chứng mờ trong 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 đến stdout (nếu chưa được đặt)

Chất lượng
cải thiện tính dễ đọc của các điều khoản bằng chứng được tạo ra bởi một số chiến thuật

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