coqide.byte - Online di Cloud

PROGRAM:

NAMA

coqide - Antarmuka grafis Coq Proof Assistant

RINGKASAN

coqide [ Pilihan ]

DESKRIPSI

coqide adalah antarmuka grafis gtk untuk asisten bukti Coq.

Untuk penggunaan Coq berorientasi baris perintah, lihat coqtop(1) ; untuk penggunaan Coq berorientasi batch, lihat
coqc(1).

PILIHAN

-h Tampilkan daftar lengkap opsi yang diterima oleh coqide.

-I dir, -termasuk dir
Tambahkan dir direktori di jalur sertakan.

-R dir coqdir
Memetakan fisik secara rekursif dir untuk logis coqdir.

-src Tambahkan direktori sumber di jalur sertakan.

-adalah f, -keadaan masukan f
Baca status dari f.coq.

-kebisingan Mulailah dengan keadaan kosong.

-keadaan keluaran f
Tulis status dalam file f.coq.

-load-ml-objek f
Muat file objek ML f.

-load-ml-sumber f
Muat file ML f.

-l f, -muat-vernac-sumber f
Muat file Coq f.v (Muat f.).

-lv f, -memuat-vernac-sumber-verbose f
Muat file Coq f.v (Muat Verbose f.).

-muat-verna-objek f
Muat file objek Coq f.vo.

-memerlukan f
Muat file objek Coq f.vo dan impor (Memerlukan f.).

-menyusun f
Kompilasi file Coq f.v (menyiratkan -kelompok).

-kompilasi-verbose f
Kompilasi file Coq dengan benar f.v (menyiratkan -kelompok).

-memilih Jalankan versi kode asli Coq atau Coq_SearchIsos.

-byte Jalankan versi bytecode Coq atau Coq_SearchIsos.

-di mana Cetak lokasi perpustakaan standar Coq dan keluar.

-v Cetak versi Coq dan keluar.

-q Lewati pemuatan rcfile.

-init-file f
Setel rcfile ke f.

-kelompok Mode batch (keluar tepat setelah penguraian argumen).

-boot Mode boot (menyiratkan -q dan -kelompok).

-emac Memberitahu Coq bahwa itu dieksekusi di bawah Emacs.

-dump-glob f
Buang globalisasi dalam file f (untuk digunakan oleh coqdoc(1)).

-impredikatif-set
Setel pengurutan Setel impredikatif.

-jangan-memuat-bukti
Jangan memuat bukti buram dalam memori.

-xml Ekspor file XML baik ke hierarki yang berakar di direktori
COQ_XML_LIBRARY_ROOT (jika disetel) atau ke stdout (jika tidak disetel).

Gunakan coqide.byte online menggunakan layanan onworks.net