これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、または MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド coqtop です。
プログラム：
NAME
coqtop - Coq Proof Assistant のトップレベル システム
SYNOPSIS
コクトップ [ オプション ]
DESCRIPTION
コクトップ 対話的に使用するための Coq のトップレベル システムです。 上のフレーズを読み上げます
標準入力を使用し、結果を標準出力に出力します。
Coq のバッチ指向の使用については、を参照してください。 コックとします。
OPTIONS
-NS、 - 助けて
ヘルプ。 coqtop が受け入れるオプションの完全なリストが表示されます。
-I 監督、 - 含む DIR
ディレクトリを追加する DIR インクルードパス内
-R DIR コクディル
再帰的に物理的にマップする DIR 論理的に コクディル
-上 コクディル
トップレベル名を次のように設定します コクディル トップの代わりに
-入力状態 ファイル名、 -です ファイル名
ファイルから状態を読み取る ファイル名.coq
-ノイズ 空の初期状態から開始する
-出力状態ファイル名
状態をファイルに書き込む ファイル名.coq
-load-ml-オブジェクト ファイル名
MLオブジェクトファイルをロードする ファイル名
-load-ml-ソース ファイル名
MLファイルをロードする ファイル名
-load-vernac-ソース ファイル名、 -l ファイル名
Coqファイルをロードする ファイル名.v (ファイル名をロードします。)
-load-vernac-source-verbose ファイル名、 -lv ファイル名
Coq ファイルを詳細にロードする ファイル名.v (詳細なファイル名をロードします。)
-load-vernac-object ファイル名
Coq オブジェクト ファイルをロードする ファイル名.vo
-必須 ファイル名
Coq オブジェクト ファイルをロードする ファイル名.vo そしてそれをインポートします (インポートファイル名が必要です)。
-コンパイル ファイル名
Coqファイルをコンパイルする ファイル名.v （示す -バッチ )
-コンパイル-冗長 ファイル名
Coq ファイルを詳細にコンパイルする ファイル名.v （示す -バッチ )
-選択する Coq のネイティブ コード バージョンを実行する
-バイト Coq のバイトコード バージョンを実行する
-どこ Coq の標準ライブラリの場所を出力して終了します
-v Coq バージョンを出力して終了します
-q rcfileのロードをスキップする
-init-ファイル ファイル名
rcfileを次のように設定します ファイル名
-バッチ バッチモード (引数の解析直後に終了)
-ブート ブートモード（暗黙的に -q & -バッチ )
-emacs Emacs で実行されることを Coq に伝えます
-ダンプグロブ ファイル名
ファイル f にグローバリゼーションをダンプします (によって使用されます) コクドック(1) )
-ジオプルーフ付き (はい|いいえ)
Coqide 内の Geoproof の特別な機能を有効化 (無効化) します (デフォルトは はい )
-impredicative-set
set sort 述語を設定する
-ドントロードプルーフ
不透明なプルーフをメモリにロードしないでください
-xml XML ファイルをディレクトリをルートとする階層にエクスポートします。
$COQ_XML_LIBRARY_ROOT (設定されている場合) または stdout (未設定の場合)
品質
いくつかの戦術によって生成された証明項の読みやすさを向上させる
onworks.net サービスを使用してオンラインで coqtop を使用する
