coq-tex - מקוון בענן

תָכְנִית:

שֵׁם

coq-tex - עיבוד ביטויי Coq המוטמעים בקבצי LaTeX

תַקצִיר

coq-tex [ -o קובץ פלט ] [ -n רוחב קו ] [ -תמונה coq-image ] [ -w ] [ -v ] [ -סל ] [
-הרולה ] [ -קָטָן ] קובץ קלט ...

תיאור

השמיים coq-tex מסנן מחלץ ביטויי 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' מצורף.

הקבצים שהופקו על ידי coq-tex ניתן לעבד ישירות על ידי LaTeX. שני ביטויי Coq
והפלט ברמה העליונה מוגדרים בגופן של מכונת כתיבה.

אפשרויות

-o קובץ פלט
ציין את שם הקובץ שבו יש לאחסן את הפלט של LaTeX. מקף `-'
גורם לפלט LaTeX להיות מודפס על פלט סטנדרטי.

-n רוחב קו
הגדר את רוחב הקו. ברירת המחדל היא 72 תווים. התגובות של הדרג העליון
הלולאה מקופלת אם הם ארוכים מרוחב הקו. לא מבוצע קיפול על
טקסט הקלט Coq.

-תמונה coq-image
גורם לקובץ coq-image להורג כדי להעריך את ביטויי Coq. כברירת מחדל,
זו הפקודה coqtop מבלי לציין נתיב כלשהו המשמש להערכה
ביטויי Coq.

-w גרם לקפל קווים על תו רווח במידת האפשר, תוך הימנעות מחיתוך מילים
בפלט. כברירת מחדל, קיפול מתרחש ברוחב הקו, ללא קשר למילה
חתכים.

-v מצב מילולי. מדפיס את תשובות ה-Coq על הפלט הסטנדרטי. שימושי לזיהוי
שגיאות בביטויי Coq.

-סל מצב משופע. תשובות Coq כתובות בגופן משופע.

-הרולה מצב קווים אופקיים. חלקי Coq כתובים בין שני קווים אופקיים.

-קָטָן מצב גופן קטן. חלקי Coq כתובים בפונט קטן יותר.

מערות

הביטויים \begin... ו-\end... חייבים לשבת על שורה בפני עצמם, ללא תווים
לפני הנטוי האחורי או אחרי הסד הסוגר. כל ביטוי Coq חייב להסתיים על ידי
`.' בסוף שורה. מתקבל רווח ריק בין `.' והקו החדש, אבל כל
תו אחר יגרום ל-coq-tex להתעלם מהסוף של הביטוי, וכתוצאה מכך א
ערבוב שגוי של התגובות לתוך הביטויים. (התגובות ``משוכות מאחור`').

השתמש ב-coq-tex באינטרנט באמצעות שירותי onworks.net