coqtop - Dalam talian di Awan

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