Это команда coqc, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
coqc - компилятор Coq Proof Assistant
СИНТАКСИС
кокс [ Генеральная кран кредита ] файл
ОПИСАНИЕ
кокс - пакетный компилятор для Coq Proof Assistant. Варианты в основном
так же, как Coqtop(1). файл.v файл на местном языке для компиляции. файл должен быть сформирован только
с символами от «a» до «Z», «0» - «9» или «_» и должен начинаться с буквы. В
компилятор создает объектный файл файл.vo.
Для интерактивного использования Coq см. Coqtop(1).
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
кокс это скрипт, который просто запускает Coqtop с опцией -компилировать он принимает те же варианты
as коктоп.
-образ бункер
использование бункер как основа Coqtop вместо стандартного.
-подробный
распечатать скомпилированный файл на стандартный вывод.
Используйте coqc онлайн с помощью сервисов onworks.net
