これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、または MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド gallina です。
プログラム：
NAME
gallina - Coq の言語ファイルから仕様を抽出します
SYNOPSIS
めんどり [ - ] [ -標準出力 ] [ -コメントはありません ] file ...
DESCRIPTION
めんどり Coq ファイルを引数として受け取り、対応する仕様ファイルを構築します。
Coq ファイル foo.v 仕様ファイルに記載します foo.g。 接尾辞「.g」は
ガリーナのために。
そのために、gallina は「定理」、「補題」、「事実」に続くすべてのコマンドを削除します。
コマンド「中止」、「保存」、「終了」に達するまでの「コメント」または「目標」ステートメント
「決まった。」 または「証明 <...>」。 また、すべての「ヒント」、「構文」、「即時」、または
「透明」コマンド。
.v 接尾辞のないファイルは無視されます。
OPTIONS
-標準出力
結果を標準出力に出力します。
- Coq ソースは標準入力で取得されます。 結果は標準出力に出力されます。
-コメントはありません
*.g ファイル内のコメントは削除されます。
注意事項
ネストされたコメントは正しく処理されます。 特に、すべてのコマンド「保存」。 または「中止」。 で
コメントは考慮されません。
onworks.net サービスを使用してオンラインで gallina を使用する
