Este é o comando coqc que pode ser executado no provedor de hospedagem gratuita OnWorks usando uma de nossas várias estações de trabalho online gratuitas, como Ubuntu Online, Fedora Online, emulador online do Windows ou emulador online do MAC OS
PROGRAMA:
NOME
coqc - O compilador Coq Proof Assistant
SINOPSE
coqc [ geral galo opções ] lima
DESCRIÇÃO
coqc é o compilador em lote para o Coq Proof Assistant. As opções são basicamente
mesma coqueteleira(1). arquivo.v é o arquivo vernáculo a ser compilado. lima deve ser formado apenas
com os caracteres `a` a` Z`, `0`-`9` ou` _` e deve começar com uma letra. o
compilador produz um arquivo objeto arquivo.vo.
Para uso interativo do Coq, consulte coqueteleira(1).
OPÇÕES
coqc é um script que simplesmente executa coqueteleira com opção -compilar aceita as mesmas opções
as coqtop.
-imagem caixa
usar caixa como subjacente coqueteleira em vez do padrão.
-verboso
imprime o arquivo compilado na saída padrão.
Use coqc online usando serviços onworks.net
