Это команда coq-tex, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
coq-tex - обрабатывает фразы Coq, встроенные в файлы LaTeX
СИНТАКСИС
кок-текс [ -o выходной файл ] [ -n ширина линии ] [ -образ coq-образ ] [ -w ] [ -v ] [ -сл ] [
-руле ] [ -маленький ] входной файл ...
ОПИСАНИЕ
В кок-текс фильтр извлекает фразы 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
а выходные данные верхнего уровня набираются печатным шрифтом.
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
-o выходной файл
Укажите имя файла, в котором будет сохранен вывод LaTeX. Тире `- '
заставляет вывод LaTeX печататься на стандартном выводе.
-n ширина линии
Установите ширину линии. По умолчанию 72 символа. Ответы высшего уровня
петли складываются, если они длиннее ширины линии. Фальцовка не выполняется на
текст ввода Coq.
-образ coq-образ
Потому что файл coq-образ для выполнения для оценки фраз Coq. По умолчанию,
это команда Coqtop без указания пути, который используется для оценки
фразы Coq.
-w По возможности заставляйте строки складываться по пробелу, избегая сокращений слов
на выходе. По умолчанию сворачивание происходит по ширине линии, независимо от слова
режет.
-v Подробный режим. Печатает ответы Coq на стандартном выходе. Полезно для обнаружения
ошибки в фразах Coq.
-сл Наклонный режим. Ответы Coq написаны наклонным шрифтом.
-руле Режим горизонтальных линий. Партии Coq написаны между двумя горизонтальными линиями.
-маленький Режим мелкого шрифта. Детали Coq написаны более мелким шрифтом.
Пещеры
Фразы \ begin ... и \ end ... должны располагаться в отдельной строке, без символов.
перед обратной косой чертой или после закрывающей фигурной скобки. Каждая фраза Coq должна оканчиваться
`. ' в конце строки. Между `. 'Допускается пробел. и символ новой строки, но любой
другой символ заставит coq-tex игнорировать конец фразы, что приведет к
неправильная перетасовка ответов по фразам. (Ответы `` отстают ''.)
Используйте coq-tex онлайн с помощью сервисов onworks.net
