Ini ialah arahan coqtop 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
coqtop - Sistem peringkat atasan Pembantu Bukti Coq
SINOPSIS
coqtop [ pilihan ]
DESCRIPTION
coqtop ialah sistem peringkat teratas Coq, untuk kegunaan interaktif. Ia membaca frasa pada
input standard, dan mencetak keputusan pada output standard.
Untuk penggunaan berorientasikan kelompok Coq, lihat coqc(1).
PILIHAN
-h, - membantu
Tolong. Akan memberikan anda senarai lengkap pilihan yang diterima oleh coqtop.
-I adalah, --termasuk dir
tambah direktori dir dalam laluan termasuk
-R dir coqdir
memetakan fizikal secara rekursif dir kepada logik coqdir
-atas coqdir
tetapkan nama peringkat teratas menjadi coqdir bukannya Top
-keadaan input nama fail, -adalah nama fail
baca keadaan daripada fail nama fail.coq
-bising mulakan dengan keadaan awal yang kosong
-keadaan keluarannama fail
tulis keadaan dalam fail nama fail.coq
-beban-ml-objek nama fail
muatkan fail objek ML nama fail
-muat-ml-sumber nama fail
muatkan fail ML nama fail
-muat-sumber-vernac nama fail, -l nama fail
muatkan fail Coq nama fail.v (Muat nama fail.)
-muat-vernac-source-verbose nama fail, -lv nama fail
memuatkan fail Coq secara bertele-tele nama fail.v (Muat nama fail Verbose.)
-beban-vernac-objek nama fail
muatkan fail objek Coq nama fail.vo
-memerlukan nama fail
muatkan fail objek Coq nama fail.vo dan importnya (Memerlukan Import nama fail.)
-susun nama fail
menyusun fail Coq nama fail.v (menyiratkan -batch )
-compile-verbose nama fail
menyusun fail Coq secara lisan nama fail.v (menyiratkan -batch )
-pilih jalankan versi kod asli Coq
-bait jalankan versi bytecode Coq
-di mana cetak lokasi perpustakaan standard Coq dan keluar
-v cetak versi Coq dan keluar
-q langkau memuatkan rcfile
-init-file nama fail
tetapkan rcfile kepada nama fail
-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 nama fail
buang globalisasi dalam fail f (untuk digunakan oleh coqdoc(1) )
-dengan-geoproof (ya|tidak)
untuk (nyahaktifkan) fungsi khas untuk Geoproof dalam Coqide (lalai ialah yes )
-impredicative-set
set sort Set impredicative
-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)
Yang berkualiti
meningkatkan keterbacaan istilah pembuktian yang dihasilkan oleh beberapa taktik
Gunakan coqtop dalam talian menggunakan perkhidmatan onworks.net
