coqtop - онлайн в хмарі

ПРОГРАМА:

ІМ'Я

coqtop - система верхнього рівня Coq Proof Assistant

СИНТАКСИС

coqtop [ опції ]

ОПИС

coqtop це система верхнього рівня Coq для інтерактивного використання. Він читає фрази на
стандартного введення та друкує результати на стандартному виводі.

Для пакетного використання Coq див coqc(1).

ВАРІАНТИ

-h, --допомога
Допоможіть. Дасть вам повний список опцій, які приймає coqtop.

-I реж., --включати реж
додати каталог реж у шляху включення

-R реж coqdir
рекурсивно відображати фізичні реж до логічного coqdir

-поверх coqdir
встановити ім’я верхнього рівня coqdir замість Top

-вхідний стан ім'я файлу, -є ім'я файлу
читання стану з файлу ім'я файлу.coq

- шум почати з порожнього початкового стану

- вихідний станім'я файлу
записати стан у файл ім'я файлу.coq

-load-ml-object ім'я файлу
завантажити об’єктний файл ML ім'я файлу

-load-ml-source ім'я файлу
завантажити файл ML ім'я файлу

-load-vernac-source ім'я файлу, -l ім'я файлу
завантажити файл Coq ім'я файлу.v (Завантажити ім'я файлу.)

-load-vernac-source-verbose ім'я файлу, -лв ім'я файлу
багатослівно завантажте файл Coq ім'я файлу.v (Завантажте детальну назву файлу.)

-load-vernac-object ім'я файлу
завантажити об’єктний файл Coq ім'я файлу.vo

-вимагають ім'я файлу
завантажити об’єктний файл Coq ім'я файлу.vo та імпортуйте його (Вимагати імпорт файлу.)

-компілювати ім'я файлу
компілювати файл Coq ім'я файлу.v (припускає - партія )

-компілювати-багато ім'я файлу
детально компілювати файл Coq ім'я файлу.v (припускає - партія )

-опт запустити версію Coq з рідним кодом

-байт запустити версію Coq з байт-кодом

-де роздрукувати стандартне розташування бібліотеки Coq і вийти

-v роздрукувати версію Coq і вийти

-q пропустити завантаження rc-файлу

-ініціальний файл ім'я файлу
встановіть файл rc ім'я файлу

- партія пакетний режим (виходить відразу після розбору аргументів)

- черевик режим завантаження (мається на увазі -q та - партія )

-emacs повідомляє Coq, що він виконується під Emacs

- dump-glob ім'я файлу
дамп глобалізацій у файл f (для використання coqdoc(1) )

-з-геозащита (так|ні)
(де)активувати спеціальні функції для Geoproof в Coqide (за умовчанням так )

-імприкативний-набір
набір сортування Встановити непредикативний

-незавантаження
не завантажуйте непрозорі докази в пам'ять

-xml експортувати файли XML або в ієрархію, вкорінену в каталозі
$COQ_XML_LIBRARY_ROOT (якщо встановлено) або в стандартний вихід (якщо не встановлено)

Якості
покращити розбірливість термінів доказу, створених за допомогою деяких тактик

Використовуйте coqtop онлайн за допомогою служб onworks.net