นี่คือคำสั่ง coq-tex ที่สามารถเรียกใช้ในผู้ให้บริการโฮสต์ฟรีของ OnWorks โดยใช้หนึ่งในเวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
coq-tex - ประมวลผลวลี Coq ที่ฝังอยู่ในไฟล์ LaTeX
เรื่องย่อ
ค็อก-เท็กซ์ [ -o ไฟล์เอาต์พุต ] [ -n เส้นกว้าง ] [ -ภาพ ภาพ coq ] [ -w ] [ -v ] [ -sl ] [
-รูรูล ] [ เล็ก ] ไฟล์อินพุต ...
DESCRIPTION
การขอ ค็อก-เท็กซ์ ตัวกรองแยกวลี Coq ที่ฝังอยู่ในไฟล์ LaTeX ประเมินและ
แทรกผลการประเมินหลังแต่ละวลี
สภาพแวดล้อม LaTeX สามแบบมีให้เพื่อรวมโค้ด Coq ในไฟล์อินพุต:
coq_example
วลีระหว่าง \begin{coq_example} และ \end{coq_example} จะถูกประเมินและ
คัดลอกไปยังไฟล์ที่ส่งออก แต่ละวลีตามด้วยคำตอบของ
ลูประดับบนสุด
coq_example*
วลีระหว่าง \begin{coq_example*} และ \end{coq_example*} จะถูกประเมินและ
คัดลอกไปยังไฟล์ที่ส่งออก การตอบสนองของลูประดับบนสุดถูกยกเลิก
coq_eval
วลีระหว่าง \begin{coq_eval} และ \end{coq_eval} จะถูกประเมินอย่างเงียบๆ
พวกเขาจะไม่ถูกคัดลอกไปยังไฟล์ที่ส่งออกและการตอบสนองของลูประดับบนสุด
ถูกทิ้ง
รหัส LaTeX ที่ได้จะถูกเก็บไว้ในไฟล์ ไฟล์.v.tex ถ้าไฟล์อินพุตมีชื่อ
แบบฟอร์ม ไฟล์.tex มิฉะนั้น ชื่อของไฟล์เอาต์พุตจะเป็นชื่อของไฟล์อินพุต
โดยต่อท้าย `.v.tex'
ไฟล์ที่ผลิตโดย ค็อก-เท็กซ์ สามารถประมวลผลได้โดยตรงโดย LaTeX ทั้งวลี Coq
และเอาต์พุตระดับบนสุดเป็นแบบเรียงพิมพ์ในแบบอักษรของเครื่องพิมพ์ดีด
OPTIONS
-o ไฟล์เอาต์พุต
ระบุชื่อไฟล์ที่จะเก็บเอาต์พุต LaTeX ขีด `-'
ทำให้เอาต์พุต LaTeX ถูกพิมพ์บนเอาต์พุตมาตรฐาน
-n เส้นกว้าง
กำหนดความกว้างของเส้น ค่าเริ่มต้นคือ 72 อักขระ คำตอบของระดับบนสุด
วงจะพับถ้ายาวกว่าความกว้างของเส้น ไม่มีการพับบน
ข้อความป้อน Coq
-ภาพ ภาพ coq
สาเหตุของไฟล์ ภาพ coq ที่จะดำเนินการเพื่อประเมินวลี Coq โดยค่าเริ่มต้น,
นี่คือคำสั่ง คอคท็อป โดยไม่ระบุเส้นทางใด ๆ ที่ใช้ในการประเมิน
วลี Coq
-w ทำให้บรรทัดถูกพับบนอักขระเว้นวรรคทุกครั้งที่ทำได้ หลีกเลี่ยงการตัดคำ
ในการส่งออก ตามค่าเริ่มต้น การพับจะเกิดขึ้นที่ความกว้างของบรรทัด โดยไม่คำนึงถึง word
ตัด
-v โหมดละเอียด พิมพ์คำตอบ Coq บนเอาต์พุตมาตรฐาน มีประโยชน์ในการตรวจจับ
ข้อผิดพลาดในวลี Coq
-sl โหมดเอียง คำตอบของ Coq เขียนด้วยแบบอักษรเอียง
-รูรูล โหมดเส้นแนวนอน ส่วน Coq เขียนระหว่างเส้นแนวนอนสองเส้น
เล็ก โหมดแบบอักษรขนาดเล็ก ส่วน Coq เขียนด้วยแบบอักษรที่เล็กกว่า
คำเตือน
วลี \begin... และ \end... ต้องอยู่ในบรรทัดเดียวโดยไม่มีอักขระ
ก่อนแบ็กสแลชหรือหลังวงเล็บปีกกาปิด แต่ละวลีของ Coq ต้องสิ้นสุดโดย
`.' ที่ท้ายบรรทัด ช่องว่างระหว่าง `.' ได้รับการยอมรับ และขึ้นบรรทัดใหม่ แต่อย่างใด
อักขระอื่นจะทำให้ coq-tex ละเว้นส่วนท้ายของวลีส่งผลให้ an
การสับเปลี่ยนคำตอบเป็นวลีที่ไม่ถูกต้อง (คำตอบ ``ล้าหลัง'')
ใช้ coq-tex ออนไลน์โดยใช้บริการ onworks.net
