นี่คือคำสั่ง gallina ที่สามารถเรียกใช้ในผู้ให้บริการโฮสต์ฟรีของ OnWorks โดยใช้เวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
gallina - แยกข้อมูลจำเพาะจากไฟล์พื้นถิ่นของ Coq
เรื่องย่อ
ไก่ [ - ] [ -stdout ] [ -ไม่มีความคิดเห็น ] ไฟล์ ...
DESCRIPTION
ไก่ รับไฟล์ Coq เป็นอาร์กิวเมนต์และสร้างไฟล์ข้อกำหนดที่เกี่ยวข้อง
ไฟล์ Coq ฟู.วี ให้หมีกับไฟล์ข้อมูลจำเพาะ ฟูก. คำต่อท้าย '.g' หมายถึง
สำหรับกัลลิน่า
เพื่อจุดประสงค์นั้น แกลลินาจะลบคำสั่งทั้งหมดที่เป็นไปตาม "ทฤษฎีบท", "เล็มมา", "ข้อเท็จจริง"
คำสั่ง "หมายเหตุ" หรือ "เป้าหมาย" จนกว่าจะถึงคำสั่ง "ยกเลิก", "บันทึก", "Qed",
"กำหนด." หรือ "หลักฐาน <...>." นอกจากนี้ยังลบทุก "คำแนะนำ", "ไวยากรณ์", "ทันที" หรือ
คำสั่ง "โปร่งใส"
ไฟล์ที่ไม่มีนามสกุล .v จะถูกละเว้น
OPTIONS
-stdout
พิมพ์ผลลัพธ์บนเอาต์พุตมาตรฐาน
- แหล่ง Coq ใช้อินพุตมาตรฐาน ผลลัพธ์จะถูกพิมพ์บนเอาต์พุตมาตรฐาน
-ไม่มีความคิดเห็น
ความคิดเห็นจะถูกลบออกในไฟล์ *.g
หมายเหตุ
ความคิดเห็นที่ซ้อนกันได้รับการจัดการอย่างถูกต้อง โดยเฉพาะทุกคำสั่ง "บันทึก" หรือ "ยกเลิก" ใน
ความคิดเห็นจะไม่ถูกนำมาพิจารณา
ใช้ gallina ออนไลน์โดยใช้บริการ onworks.net