Ini adalah perintah gallina yang dapat dijalankan di penyedia hosting gratis OnWorks menggunakan salah satu dari beberapa workstation online gratis kami seperti Ubuntu Online, Fedora Online, emulator online Windows atau emulator online MAC OS
PROGRAM:
NAMA
gallina - mengekstrak spesifikasi dari file vernakular Coq
RINGKASAN
ayam [ - ] [ -stdout ] [ -tidak ada komentar ] fillet ...
DESKRIPSI
ayam mengambil file Coq sebagai argumen dan membangun file spesifikasi yang sesuai.
File Coq foo.v memberikan bantalan pada file spesifikasi foo.g. Akhiran '.g' berdiri
untuk Galina.
Untuk tujuan itu, gallina menghapus semua perintah yang mengikuti "Teorema", "Lemma", "Fakta",
Pernyataan "Remark" atau "Goal" hingga mencapai perintah "Abort.", "Save.", "Qed.",
"Ditentukan." atau "Bukti <...>.". Itu juga menghapus setiap "Petunjuk", "Sintaks", "Segera" atau
Perintah "Transparan".
File tanpa akhiran .v diabaikan.
PILIHAN
-stdout
Mencetak hasil pada output standar.
- Sumber Coq diambil pada input standar. Hasilnya dicetak pada output standar.
-tidak ada komentar
Komentar dihapus di file *.g.
CATATAN
Komentar bersarang ditangani dengan benar. Secara khusus, setiap perintah "Simpan." atau "Batalkan". di dalam
komentar tidak diperhitungkan.
Gunakan gallina online menggunakan layanan onworks.net
