coqtop - Online na nuvem

PROGRAMA:

NOME

coqtop - O sistema de nível superior Coq Proof Assistant

SINOPSE

coqueteleira [ opções ]

DESCRIÇÃO

coqueteleira é o sistema de nível superior da Coq, para uso interativo. Ele lê frases no
entrada padrão e imprime os resultados na saída padrão.

Para uso orientado a lote de Coq, consulte coqc(1).

OPÇÕES

-h, --Socorro
Ajuda. Fornecerá a lista completa de opções aceitas pelo coqtop.

-I é, --incluir dir
adicionar diretório dir no caminho de inclusão

-R dir coqdir
mapear recursivamente físico dir para lógico coqdir

-topo coqdir
defina o nome de nível superior para ser coqdir em vez de Top

-estado de entrada nome do arquivo, -é nome do arquivo
ler estado do arquivo nome do arquivo.coq

-não é comece com um estado inicial vazio

-estado de saídanome do arquivo
escrever estado no arquivo nome do arquivo.coq

-load-ml-objeto nome do arquivo
carregar arquivo de objeto ML nome de arquivo

-load-ml-fonte nome do arquivo
carregar arquivo ML nome do arquivo

-load-vernac-fonte nome do arquivo, -l nome do arquivo
carregar arquivo Coq nomedoarquivo.v (Carregar o nome do arquivo.)

-load-vernac-fonte-verbose nome do arquivo, -lv nome do arquivo
carregar arquivo Coq detalhadamente nomedoarquivo.v (Carregar nome de arquivo detalhado.)

-load-vernac-objeto nome do arquivo
carregar arquivo de objeto Coq nomedoarquivo.vo

-requer nome do arquivo
carregar arquivo de objeto Coq nomedoarquivo.vo e importe-o (Exigir nome do arquivo de importação.)

-compilar nome do arquivo
compilar arquivo Coq nomedoarquivo.v (implica -lote )

-compilar-verboso nome do arquivo
compilar detalhadamente o arquivo Coq nomedoarquivo.v (implica -lote )

-optar execute a versão de código nativo do Coq

-byte execute a versão bytecode do Coq

-Onde imprimir a localização da biblioteca padrão do Coq e sair

-v imprimir a versão Coq e sair

-q pular o carregamento do rcfile

-arquivo de inicialização nome do arquivo
defina o rcfile para nome do arquivo

-lote modo em lote (sai logo após a análise de argumentos)

-Bota modo de inicialização (implica -q e -lote )

-emacs diz ao Coq que é executado no Emacs

-dump-glob nome do arquivo
despejar globalizações no arquivo f (para ser usado por coqdoc(1) )

-com-geoproof (sim | não)
para (des) ativar funções especiais para Geoproof dentro de Coqide (o padrão é sim )

-conjunto impredicativo
definir classificação Definir impredicativo

-não-load-proofs
não carregue provas opacas na memória

-xml exportar arquivos XML para a hierarquia enraizada no diretório
$ COQ_XML_LIBRARY_ROOT (se definido) ou para stdout (se não definido)

Qualidade
melhorar a legibilidade dos termos de prova produzidos por algumas táticas

Use o coqtop online usando os serviços onworks.net