Це команда coqc, яку можна запустити в постачальнику безкоштовного хостингу OnWorks за допомогою однієї з наших численних безкоштовних робочих станцій, таких як Ubuntu Online, Fedora Online, онлайн-емулятор Windows або онлайн-емулятор MAC OS
ПРОГРАМА:
ІМ'Я
coqc - компілятор Coq Proof Assistant
СИНТАКСИС
coqc [ загальний кран опції ] файл
ОПИС
coqc є пакетним компілятором для Coq Proof Assistant. Варіанти в основному є
так само, як coqtop(1). файл.v є файлом для компіляції. файл має бути тільки сформований
із символами від `a` до `Z`, `0`-`9` або `_` і має починатися з літери. The
компілятор створює об'єктний файл file.vo.
Інтерактивне використання Coq див coqtop(1).
ВАРІАНТИ
coqc це скрипт, який просто запускається coqtop з опцією -компілювати він приймає ті самі варіанти
as coqtop.
-образ Бен
використання Бен як основне coqtop замість стандартного.
-вербозний
роздрукувати скомпільований файл на стандартному виводі.
Використовуйте coqc онлайн за допомогою служб onworks.net
