Ini ialah arahan coqide.byte yang boleh dijalankan dalam penyedia pengehosan percuma OnWorks menggunakan salah satu daripada berbilang stesen kerja dalam talian percuma kami seperti Ubuntu Online, Fedora Online, emulator dalam talian Windows atau emulator dalam talian MAC OS
JADUAL:
NAMA
coqide - Antara muka grafik Coq Proof Assistant
SINOPSIS
cokide [ pilihan ]
DESCRIPTION
cokide ialah antara muka grafik gtk untuk pembantu kalis Coq.
Untuk penggunaan berorientasikan baris arahan bagi Coq, lihat coqtop(1) ; untuk penggunaan berorientasikan kelompok Coq, lihat
coqc(1).
PILIHAN
-h Tunjukkan senarai lengkap pilihan yang diterima oleh cokide.
-I dir, -termasuk dir
Tambah dir direktori dalam laluan sertakan.
-R dir coqdir
Memetakan fizikal secara rekursif dir kepada logik coqdir.
-src Tambahkan direktori sumber dalam laluan sertakan.
-adalah f, -keadaan input f
Baca negeri dari f.coq.
-bising Mulakan dengan keadaan kosong.
-keadaan keluaran f
Tulis keadaan dalam fail f.coq.
-beban-ml-objek f
Muatkan fail objek ML f.
-muat-ml-sumber f
Muatkan fail ML f.
-l f, -muat-sumber-vernac f
Muatkan fail Coq f.v (Muat f.).
-lv f, -muat-vernac-source-verbose f
Muatkan fail Coq f.v (Muat Verbose f.).
-beban-vernac-objek f
Muatkan fail objek Coq f.vo.
-memerlukan f
Muatkan fail objek Coq f.vo dan importnya (Memerlukan f.).
-susun f
Susun fail Coq f.v (menyiratkan -batch).
-compile-verbose f
Susun fail Coq secara lisan f.v (menyiratkan -batch).
-pilih Jalankan versi kod asli Coq atau Coq_SearchIsos.
-bait Jalankan versi bytecode Coq atau Coq_SearchIsos.
-di mana Cetak lokasi perpustakaan standard Coq dan keluar.
-v Cetak versi Coq dan keluar.
-q Langkau memuatkan rcfile.
-init-file f
Tetapkan rcfile kepada f.
-batch Mod kelompok (keluar sejurus selepas hujah dihuraikan).
-but Mod but (menyiratkan -q and -batch).
-emacs Memberitahu Coq ia dilaksanakan di bawah Emacs.
-dump-glob f
Buang globalisasi dalam fail f (untuk digunakan oleh coqdoc(1)).
-impredicative-set
Tetapkan isihan Tetapkan impredikatif.
-jangan-beban-bukti
Jangan muatkan bukti legap dalam ingatan.
-xml Eksport fail XML sama ada ke hierarki yang berakar dalam direktori
COQ_XML_LIBRARY_ROOT (jika ditetapkan) atau ke stdout (jika tidak ditetapkan).
Gunakan coqide.byte dalam talian menggunakan perkhidmatan onworks.net
