Bu, Ubuntu Online, Fedora Online, Windows çevrimiçi emülatörü veya MAC OS çevrimiçi emülatörü gibi birden fazla ücretsiz çevrimiçi iş istasyonumuzdan birini kullanarak OnWorks ücretsiz barındırma sağlayıcısında çalıştırılabilen komut coqtop'tur.
Program:
ADI
coqtop - Coq Proof Assistant üst düzey sistemi
SİNOPSİS
ocak [ seçenekleri ]
TANIM
ocak etkileşimli kullanım için Coq'un en üst düzey sistemidir. üzerindeki cümleleri okur.
standart girdi ve sonuçları standart çıktıya yazdırır.
Coq'un parti odaklı kullanımı için, bkz. koklamak(1).
SEÇENEKLER
-H, --yardım et
Yardım. Size coqtop tarafından kabul edilen seçeneklerin tam listesini verecektir.
-I dir --Dahil etmek dir
dizin ekle dir dahil etme yolunda
-R dir kokdir
fiziksel haritayı özyinelemeli olarak dir mantıklı kokdir
-üst kokdir
üst düzey adı olacak şekilde ayarla kokdir Üst yerine
-giriş durumu dosya adı, -dır-dir Dosya
dosyadan durumu oku dosyaadi.coq
-gürültü boş bir başlangıç durumuyla başla
-çıktı durumuDosya
durumu dosyaya yaz dosyaadi.coq
-load-ml-nesne Dosya
ML nesne dosyasını yükle dosya adı
-load-ml-kaynak Dosya
ML dosyasını yükle Dosya
-load-vernac-kaynak dosya adı, -l Dosya
Coq dosyasını yükle dosyaadı.v (Dosya adını yükleyin.)
-load-vernac-kaynak-ayrıntılı dosya adı, -lv Dosya
ayrıntılı Coq dosyası yükle dosyaadı.v (Ayrıntılı dosya adını yükleyin.)
-load-vernac-nesne Dosya
Coq nesne dosyasını yükle dosyaadi.vo
-gerekmek Dosya
Coq nesne dosyasını yükle dosyaadi.vo ve içe aktarın (Dosya adını içe aktarın gerekli.)
-derlemek Dosya
Coq dosyasını derlemek dosyaadı.v (ima -grup )
-derleme-ayrıntılı Dosya
Coq dosyasını ayrıntılı bir şekilde derleyin dosyaadı.v (ima -grup )
-seçmek Coq'un yerel kod sürümünü çalıştırın
-bayt Coq'un bayt kodu sürümünü çalıştırın
-nerede Coq'un standart kitaplık konumunu yazdırın ve çıkın
-v Coq sürümünü yazdır ve çık
-q rcfile yüklemesini atla
-init-dosyası Dosya
rcfile'ı şuna ayarla Dosya
-grup toplu iş modu (argümanların ayrıştırılmasından hemen sonra çıkar)
-çizme önyükleme modu (yani -q ve -grup )
-emaclar Coq'a Emacs altında yürütüldüğünü söyler
-dump-glob Dosya
küreselleştirmeleri f dosyasına dökün (kullanmak için coqdoc(1) )
-geoproof ile (evet|hayır)
Coqide içinde Geoproof için özel işlevleri etkinleştirmek (devre dışı bırakmak) için (varsayılan Evet )
-öngörülü-küme
sıralamayı ayarla Tahmini ayarla
-yükleme-kanıtları
opak provaları belleğe yüklemeyin
-xml XML dosyalarını dizinde kök salmış hiyerarşiye dışa aktarın
$COQ_XML_LIBRARY_ROOT (ayarlanmışsa) veya stdout'a (ayarlanmamışsa)
Kalitede
bazı taktikler tarafından üretilen ispat terimlerinin okunaklılığını geliştirmek
onworks.net hizmetlerini kullanarak coqtop'u çevrimiçi kullanın