นี่คือคำสั่ง coqtop ที่สามารถเรียกใช้ในผู้ให้บริการโฮสต์ฟรีของ OnWorks โดยใช้เวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
coqtop - ระบบระดับบนสุดของ Coq Proof Assistant
เรื่องย่อ
คอคท็อป [ ตัวเลือก ]
DESCRIPTION
คอคท็อป เป็นระบบระดับบนสุดของ Coq สำหรับการใช้งานเชิงโต้ตอบ มันอ่านวลีเกี่ยวกับ
อินพุตมาตรฐาน และพิมพ์ผลลัพธ์บนเอาต์พุตมาตรฐาน
สำหรับการใช้ Coq แบบกลุ่ม โปรดดูที่ ค็อกซี(1)
OPTIONS
-ชม, --ช่วยด้วย
ช่วย. จะแสดงรายการตัวเลือกทั้งหมดที่ coqtop ยอมรับ
-I ผบ. --รวม dir
เพิ่มไดเรกทอรี dir ในเส้นทางรวม
-R dir ค็อกเดียร์
ทำซ้ำแผนที่ทางกายภาพ dir เป็นตรรกะ ค็อกเดียร์
-TOP ค็อกเดียร์
ตั้งชื่อระดับบนสุดเป็น ค็อกเดียร์ แทนท็อป
-อินพุตสถานะ ชื่อไฟล์, -คือ ชื่อไฟล์
อ่านสถานะจากไฟล์ ชื่อไฟล์.coq
- เสียงรบกวน เริ่มต้นด้วยสถานะเริ่มต้นที่ว่างเปล่า
-สถานะเอาท์พุทชื่อไฟล์
สถานะการเขียนในไฟล์ ชื่อไฟล์.coq
-load-ml-วัตถุ ชื่อไฟล์
โหลดไฟล์อ็อบเจ็กต์ ML ชื่อไฟล์
-load-ml-แหล่งที่มา ชื่อไฟล์
โหลดไฟล์ ML ชื่อไฟล์
-load-vernac-แหล่งที่มา ชื่อไฟล์, -l ชื่อไฟล์
โหลดไฟล์ Coq ชื่อไฟล์.v (โหลดชื่อไฟล์.)
-load-vernac-source-verbose ชื่อไฟล์, -เลเวล ชื่อไฟล์
โหลดไฟล์ Coq อย่างละเอียด ชื่อไฟล์.v (โหลดชื่อไฟล์อย่างละเอียด)
-load-vernac-วัตถุ ชื่อไฟล์
โหลดไฟล์อ็อบเจ็กต์ Coq ชื่อไฟล์.vo
-จำเป็นต้อง ชื่อไฟล์
โหลดไฟล์อ็อบเจ็กต์ Coq ชื่อไฟล์.vo และนำเข้า (ต้องนำเข้าชื่อไฟล์)
-รวบรวม ชื่อไฟล์
คอมไพล์ไฟล์ Coq ชื่อไฟล์.v (หมายถึง -แบทช์ )
-คอมไพล์-verbose ชื่อไฟล์
รวบรวมไฟล์ Coq อย่างละเอียด ชื่อไฟล์.v (หมายถึง -แบทช์ )
-เลือก เรียกใช้ Coq . เวอร์ชันรหัสเนทีฟ
-ไบต์ รันเวอร์ชัน bytecode ของCoq
-ที่ไหน พิมพ์ตำแหน่งห้องสมุดมาตรฐานของ Coq และทางออก
-v พิมพ์ Coq version และ exit
-q ข้ามการโหลด rcfile
-init-ไฟล์ ชื่อไฟล์
ตั้งค่า rcfile เป็น ชื่อไฟล์
-แบทช์ โหมดแบตช์ (ออกหลังจากแยกวิเคราะห์อาร์กิวเมนต์)
- บูต โหมดบูต (หมายถึง -q และ -แบทช์ )
-emac บอก Coq ว่าถูกดำเนินการภายใต้ Emacs
-dump-โลก ชื่อไฟล์
ดัมพ์ globalizations ในไฟล์ f (เพื่อใช้โดย ค็อกด็อก(1) )
-พร้อม geoproof (ใช่|ไม่ใช่)
เพื่อ (de) เปิดใช้งานฟังก์ชันพิเศษสำหรับ Geoproof ภายใน Coqide (ค่าเริ่มต้นคือ ใช่ )
-impredicative-ชุด
ตั้งค่าการเรียงลำดับ ตั้งค่า impredicative
-ไม่โหลดหลักฐาน
อย่าโหลดหลักฐานทึบแสงในหน่วยความจำ
-xml เอ็กซ์พอร์ตไฟล์ XML ไปยังลำดับชั้นที่รูทในไดเร็กทอรี
$COQ_XML_LIBRARY_ROOT (หากตั้งค่าไว้) หรือไปยัง stdout (หากไม่ได้ตั้งค่า)
ที่มีคุณภาพ
ปรับปรุงความชัดเจนของเงื่อนไขการพิสูจน์ที่สร้างโดยกลวิธีบางอย่าง
ใช้ coqtop ออนไลน์โดยใช้บริการ onworks.net