coq-tex - онлайн у хмарі

ПРОГРАМА:

ІМ'Я

coq-tex - обробляйте фрази Coq, вбудовані у файли LaTeX

СИНТАКСИС

coq-tex [ -o вихідний файл ] [ -n ширина лінії ] [ -образ coq-образ ] [ -w ] [ -v ] [ -сл ] [
-хруле ] [ -малий ] вхідний файл ...

ОПИС

Команда coq-tex filter витягує фрази Coq, вбудовані у файли LaTeX, оцінює їх та
після кожної фрази вставте результат оцінювання.

Для включення коду Coq у вхідні файли передбачено три середовища LaTeX:

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-образ
Викликати файл coq-образ виконуватися, щоб оцінити фрази Coq. За замовчуванням,
це команда coqtop без вказівки шляху, який використовується для оцінки
фрази Coq.

-w Створюйте рядки на пробілі, коли це можливо, уникаючи скорочень слів
на виході. За замовчуванням згортання відбувається на ширині лінії, незалежно від слова
порізи.

-v Детальний режим. Друкує відповіді Coq на стандартному виводі. Корисно для виявлення
помилки у фразах Coq.

-сл Похилий режим. Відповіді Coq написані похилим шрифтом.

-хруле Режим горизонтальних ліній. Частини Coq написані між двома горизонтальними рядками.

-малий Режим дрібного шрифту. Частини Coq написані меншим шрифтом.

ПЕРЕКЛАДИ

Фрази \begin... і \end... повинні розташовуватися на рядку окремо, без символів
перед зворотною косою рискою або після закриваючої дужки. Кожна фраза Coq має закінчуватися символом
`.' в кінці рядка. Між `.' допускається пробіл. і новий рядок, але будь-який
інший символ змусить coq-tex ігнорувати кінець фрази, що призведе до an
неправильне перетасування відповідей у ​​фрази. (Відповіді «відстають».)

Використовуйте coq-tex онлайн за допомогою служб onworks.net