Este é o comando coqide.byte 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
coqide - A interface gráfica do Coq Proof Assistant
SINOPSE
coque [ opções ]
DESCRIÇÃO
coque é uma interface gráfica gtk para o assistente de prova Coq.
Para o uso orientado para linha de comando do Coq, consulte coqueteleira(1); para uso orientado a lote de Coq, consulte
coqc(1).
OPÇÕES
-h Mostra a lista completa de opções aceitas por coque.
-I dir, -incluir dir
Adicione o diretório dir no caminho de inclusão.
-R dir coqdir
Mapear recursivamente físico dir para lógico coqdir.
-src Adicione diretórios de origem no caminho de inclusão.
-é f, -estado de entrada f
Ler estado de f.coq.
-não é Comece com um estado vazio.
-estado de saída f
Gravar estado no arquivo f.coq.
-load-ml-objeto f
Carregar arquivo de objeto ML f.
-load-ml-fonte f
Carregar arquivo ML f.
-l f, -load-vernac-fonte f
Carregar arquivo Coq f.v (Carregar f.).
-lv f, -load-vernac-fonte-verbose f
Carregar arquivo Coq f.v (Carregar Detalhado f.).
-load-vernac-objeto f
Carregar arquivo de objeto Coq f.vo.
-requer f
Carregar arquivo de objeto Coq f.vo e importá-lo (requer f.).
-compilar f
Compilar arquivo Coq f.v (implica -lote).
-compilar-verboso f
Compilar detalhadamente o arquivo Coq f.v (implica -lote).
-optar Execute a versão de código nativo de Coq ou Coq_SearchIsos.
-byte Execute a versão bytecode de Coq ou Coq_SearchIsos.
-Onde Imprima a localização da biblioteca padrão do Coq e saia.
-v Imprima a versão Coq e saia.
-q Ignore o carregamento do rcfile.
-arquivo de inicialização f
Defina o rcfile para f.
-lote Modo em lote (sai logo após a análise dos argumentos).
-Bota Modo de inicialização (implica -q e -lote).
-emacs Diz ao Coq que ele é executado no Emacs.
-dump-glob f
Despejar globalizações no arquivo f (para ser usado por coqdoc(1)).
-conjunto impredicativo
Definir classificação Definir impredicativo.
-não-load-proofs
Não carregue provas opacas na memória.
-xml Exporte arquivos XML para a hierarquia enraizada no diretório
COQ_XML_LIBRARY_ROOT (se configurado) ou para stdout (se não configurado).
Use coqide.byte online usando serviços onworks.net
