InglêsFrancêsEspanhol

favicon do OnWorks

coqide.byte - Online na nuvem

Execute coqide.byte no provedor de hospedagem gratuita OnWorks no Ubuntu Online, Fedora Online, emulador online do Windows ou emulador online do MAC OS

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


Servidores e estações de trabalho gratuitos

Baixar aplicativos Windows e Linux

  • 1
    greve
    greve
    Projeto Strikr Software Livre. Artefatos
    lançado sob uma 'intenção baseada'
    licença dupla: AGPLv3 (comunidade) e
    CC-BY-NC-ND 4.0 internacional
    (comercial)...
    Baixar strikr
  • 3
    GIFLIB
    GIFLIB
    giflib é uma biblioteca para leitura e
    escrevendo imagens gif. É API e ABI
    compatível com libungif que estava em
    uso amplo enquanto a compressão LZW
    algoritmo foi...
    Baixar GIFLIB
  • 4
    Alt-F
    Alt-F
    Alt-F fornece um código-fonte livre e aberto
    firmware alternativo para o DLINK
    DNS-320/320L/321/323/325/327L and
    DNR-322L. Alt-F tem Samba e NFS;
    suporta ext2 / 3/4 ...
    Baixar Alt-F
  • 5
    usm
    usm
    Usm é um pacote de slackware unificado
    gerenciador que lida automaticamente
    resolução de dependência. Ele unifica
    vários repositórios de pacotes, incluindo
    slackware, folgado, p...
    baixar usm
  • 6
    Chart.js
    Chart.js
    Chart.js é uma biblioteca Javascript que
    permite que designers e desenvolvedores desenhem
    todos os tipos de gráficos usando o HTML5
    elemento de tela. Chart js oferece uma ótima
    variedade ...
    Baixar Chart.js
  • Mais "

Comandos Linux

Ad