Это команда coqide, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
coqide - графический интерфейс Coq Proof Assistant
СИНТАКСИС
Coqide [ кредита ]
ОПИСАНИЕ
Coqide - это графический интерфейс gtk для помощника по проверке доказательств Coq.
Для использования Coq, ориентированного на командную строку, см. Coqtop(1); для пакетного использования Coq см.
кокс(1).
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
-h Показать полный список вариантов, принятых Coqide.
-I директория, -включают директория
Добавьте каталог dir в путь включения.
-R директория Coqdir
Рекурсивно отображать физический директория логично Coqdir.
-источник Добавьте исходные каталоги в путь включения.
-является f, -вводное состояние f
Прочитать состояние из f.coq.
-шум Начните с пустого состояния.
-выходное состояние f
Записать состояние в файл f.coq.
-load-ml-объект f
Загрузить объектный файл ML f.
-load-ml-источник f
Загрузить файл ML f.
-l f, -загрузить-вернак-источник f
Загрузить файл Coq f.v (Загрузить f.).
-лв f, -load-vernac-источник-подробный f
Загрузить файл Coq f.v (Загрузить подробный f.).
-загрузить-вернак-объект f
Загрузить объектный файл Coq f.во.
-требовать f
Загрузить объектный файл Coq f.vo и импортируйте его (Требуется f.).
-компилировать f
Скомпилировать файл Coq f.v (подразумевает -партия).
-компилировать подробный f
Подробно скомпилировать файл Coq f.v (подразумевает -партия).
-опт Запустите версию Coq или Coq_SearchIsos с собственным кодом.
-байт Запустите версию Coq или Coq_SearchIsos с байт-кодом.
-где Распечатайте стандартное расположение библиотеки Coq и выйдите.
-v Распечатайте версию Coq и выйдите.
-q Пропустить загрузку rcfile.
-init-файл f
Установите rcfile на f.
-партия Пакетный режим (выходит сразу после разбора аргументов).
-загрузка Режим загрузки (подразумевает -q и -партия).
-emacs Сообщает Coq, что он выполняется под Emacs.
-dump-glob f
Дамп глобализации в файл f (для использования кокдок(1 г.)).
-impredicative-набор
Установить сортировку Установить предикативный.
-Dont-load-proofs
Не загружайте непрозрачные доказательства в память.
-xml Экспорт файлов XML либо в иерархию с корнем в каталоге
COQ_XML_LIBRARY_ROOT (если установлено) или в стандартный вывод (если не установлено).
Используйте coqide онлайн с помощью сервисов onworks.net
