ນີ້ແມ່ນຄໍາສັ່ງ gallina ທີ່ສາມາດດໍາເນີນການໄດ້ໃນ OnWorks ຜູ້ໃຫ້ບໍລິການໂຮດຕິ້ງຟຣີໂດຍໃຊ້ຫນຶ່ງໃນຫຼາຍບ່ອນເຮັດວຽກອອນໄລນ໌ຂອງພວກເຮົາເຊັ່ນ Ubuntu Online, Fedora Online, Windows online emulator ຫຼື MAC OS online emulator
ໂຄງການ:
NAME
gallina - ສະກັດຂໍ້ມູນສະເພາະຈາກໄຟລ໌ Coq vernacular
ສະຫຼຸບສັງລວມ
hen [ - ] [ -stdout ] [ -ບໍ່ມີຄວາມຄິດເຫັນ ] ເອກະສານ ...
ລາຍລະອຽດ
hen ເອົາໄຟລ໌ Coq ເປັນການໂຕ້ຖຽງແລະສ້າງໄຟລ໌ສະເພາະທີ່ສອດຄ້ອງກັນ.
ໄຟລ໌ Coq foo.v ໃຫ້ bearth ກັບໄຟລ໌ສະເພາະ foo.g. ຄຳຕໍ່ທ້າຍ '.g' ຢືນຢູ່
ສໍາລັບ Gallina.
ສໍາລັບຈຸດປະສົງນັ້ນ, gallina ເອົາຄໍາສັ່ງທັງຫມົດທີ່ປະຕິບັດຕາມ "ທິດສະດີ", "Lemma", "Fact",
"ຫມາຍເຫດ" ຫຼື "ເປົ້າຫມາຍ" ຄໍາສັ່ງຈົນກ່ວາມັນບັນລຸຄໍາສັ່ງ "Abort.", "Save", "Qed.",
"ກໍານົດ." ຫຼື "ຫຼັກຖານ <...>." ມັນຍັງເອົາທຸກໆ "Hint", "Syntax", "ທັນທີ" ຫຼື
ຄໍາສັ່ງ "ໂປ່ງໃສ".
ໄຟລ໌ທີ່ບໍ່ມີຄຳຕໍ່ທ້າຍ .v ແມ່ນຖືກລະເລີຍ.
OPTIONS
-stdout
ພິມຜົນໄດ້ຮັບຕາມມາດຕະຖານ.
- ແຫຼ່ງ Coq ຖືກປະຕິບັດກັບການປ້ອນຂໍ້ມູນມາດຕະຖານ. ຜົນໄດ້ຮັບແມ່ນພິມຢູ່ໃນຜົນຜະລິດມາດຕະຖານ.
-ບໍ່ມີຄວາມຄິດເຫັນ
ຄຳເຫັນຖືກລຶບໃນໄຟລ໌ *.g.
ຫມາຍເຫດ
ຄຳເຫັນທີ່ຊ້ອນກັນຖືກຈັດການຢ່າງຖືກຕ້ອງ. ໂດຍສະເພາະ, ທຸກໆຄໍາສັ່ງ "Save." ຫຼື "ເອົາລູກອອກ." ໃນ
ຄໍາຄິດຄໍາເຫັນບໍ່ໄດ້ຖືກພິຈາລະນາ.
ໃຊ້ gallina ອອນໄລນ໌ໂດຍໃຊ້ບໍລິການ onworks.net
