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