Это команда gallina, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
gallina - извлекает спецификацию из файлов Coq на местном языке
СИНТАКСИС
курица [ - ] [ -стандартный вывод ] [ -без комментариев ] файл ...
ОПИСАНИЕ
курица принимает файлы Coq в качестве аргументов и создает соответствующие файлы спецификаций.
Файл Coq фу.в дает ссылку на файл спецификации фу.г. Суффикс .g означает
для Галлины.
Для этого галлина удаляет все команды, следующие за «Теоремой», «Леммой», «Факт»,
Оператор «Замечание» или «Цель», пока не дойдет до команды «Прервать.», «Сохранить», «Qed.»,
"Определенный." или «Доказательство <...>.». Он также удаляет все «Подсказки», «Синтаксисы», «Непосредственные» или
«Прозрачная» команда.
Файлы без суффикса .v игнорируются.
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
-стандартный вывод
Выводит результат на стандартный вывод.
- Исходный код Coq взят на стандартный ввод. Результат выводится на стандартный вывод.
-без комментариев
Комментарии удаляются в файле * .g.
ПРИМЕЧАНИЯ
Вложенные комментарии обрабатываются правильно. В частности, каждая команда «Сохранить». или «Прервать». в
комментарий не принимается во внимание.
Используйте gallina онлайн с помощью сервисов onworks.net
