англійськафранцузькаіспанська

Значок OnWorks

coqide.byte - онлайн у хмарі

Запустіть coqide.byte у постачальника безкоштовного хостингу OnWorks через Ubuntu Online, Fedora Online, онлайн-емулятор Windows або онлайн-емулятор MAC OS

Це команда coqide.byte, яку можна запустити в постачальнику безкоштовного хостингу OnWorks за допомогою однієї з наших численних безкоштовних робочих станцій, таких як Ubuntu Online, Fedora Online, онлайн- емулятор Windows або онлайн емулятор MAC OS

ПРОГРАМА:

ІМ'Я


coqide - графічний інтерфейс Coq Proof Assistant

СИНТАКСИС


coqide [ опції ]

ОПИС


coqide це графічний інтерфейс gtk для помічника Coq proof.

Про використання Coq, орієнтованого на командний рядок, див coqtop(1) ; щодо пакетного використання Coq див
coqc(1).

ВАРІАНТИ


-h Показати повний список варіантів, які приймає coqide.

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

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

-src Додайте вихідні каталоги в шлях включення.

f, -вхідний стан f
Читати стан з f.coq.

- шум Почніть з порожнього стану.

- вихідний стан f
Записати стан у файл f.coq.

-load-ml-object f
Завантажити об’єктний файл ML f.

-load-ml-source f
Завантажити файл ML f.

-l f, -load-vernac-source f
Завантажте файл Coq f.v (Завантажити f).

-лв f, -load-vernac-source-verbose f
Завантажте файл Coq f.v (дослівне завантаження f).

-load-vernac-object f
Завантажте об’єктний файл Coq f.vo.

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

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

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

-опт Запустіть версію Coq або Coq_SearchIsos з рідним кодом.

-байт Запустіть версію байт-коду Coq або Coq_SearchIsos.

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

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

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

-ініціальний файл f
Встановіть файл rc f.

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

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

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

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

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

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

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

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


Безкоштовні сервери та робочі станції

Завантажте програми для Windows і Linux

  • 1
    Панель інструментів для Java/JTOpen
    Панель інструментів для Java/JTOpen
    IBM Toolbox для Java / JTOpen є a
    бібліотека класів Java, що підтримують
    програмування клієнт/сервер та Інтернет
    моделі до системи під керуванням OS/400,
    i5/OS, o...
    Завантажте Toolbox для Java/JTOpen
  • 2
    D3.js
    D3.js
    D3.js (або D3 для документів, керованих даними)
    це бібліотека JavaScript, яка дозволяє вам
    створювати динамічні інтерактивні дані
    візуалізації у веб-браузерах. З D3
    ти ...
    Завантажити D3.js
  • 3
    Тіні
    Тіні
    Швидкий тунельний проксі, який вам допоможе
    обхід брандмауерів Це програма
    з якого також можна отримати
    https://sourceforge.net/projects/shadowsocksgui/.
    Це ха...
    Завантажити Shadowsocks
  • 4
    Теми GLPI
    Теми GLPI
    Завантажити випуск за адресою
    https://github.com/stdonato/glpi-modifications/
    Колірні теми для GLPI 0.84 і 0.85 Новинка
    Модифікації для GLPI Це
    додаток, що c...
    Завантажте теми GLPI
  • 5
    SMPlayer
    SMPlayer
    SMPlayer - це безкоштовний медіаплеєр для
    Windows і Linux з вбудованими кодеками
    який також може відтворювати відео YouTube. один
    з найцікавіших особливостей
    SMPlayer:...
    Завантажити SMPlayer
  • 6
    AAX в MP3
    AAX в MP3
    Використання: - Встановіть Audible Manager
    і відкрийте файл свого облікового запису. - Підпишіть
    у ваш аудіоаккаунт (у
    додаток). Тепер програма може
    перетворити тебе...
    Завантажити AAX в MP3
  • Детальніше »

Команди Linux

Ad