coqdoc - Online na nuvem

PROGRAMA:

NOME

coqdoc - Uma ferramenta de documentação para o assistente de prova Coq

SINOPSE

coqdoc [ opções ] arquivos

DESCRIÇÃO

coqdoc é uma ferramenta de documentação para o assistente de prova Coq. Ele cria LaTeX ou HTML
documentos de um conjunto de arquivos Coq. Veja o manual de referência do Coq para documentação (url
abaixo).

OPÇÕES

No geral opções
-h Ajuda. Fornecerá a lista completa de opções aceitas pelo coqdoc.

--html Selecione uma saída HTML.

--látex
Selecione uma saída LATEX.

--dvi Selecione uma saída DVI.

--ps Selecione uma saída PostScript.

--texmacs
Selecione uma saída TeXmacs.

--stdout
Redirecione a saída para stdout

-o arquivo,--resultado lima
Redirecione a saída para o arquivo arquivo.

-d é, --diretório dir
Arquivos de saída para o diretório dir em vez do diretório atual (a opção -d não
altere o nome do arquivo especificado com a opção -o, se houver).

-sim, --baixo
Não insira títulos para os arquivos. O comportamento padrão é inserir um título como
`` Biblioteca Foo '' para cada arquivo.

-t corda, --título corda
Defina o título do documento.

--apenas o corpo
Suprima o cabeçalho e o trailer do documento final. Assim, você pode inserir o
documento resultante em um maior.

-p corda, --preâmbulo corda
Insira algum material no preâmbulo do LATEX, logo antes de \ begin {document}
(sem sentido com -html).

--vernac-arquivo arquivo, --arquivo-tex lima
Considera o arquivo `arquivo 'respectivamente como um arquivo .v (ou .g) ou um arquivo .tex.

--arquivos-de lima
Leia os nomes dos arquivos para processar no arquivo `arquivo 'como se fossem dados no comando
linha. Útil para fontes de programas divididas em vários diretórios.

-q, --quieto
Fique quieto. Não imprima nada, exceto erros.

-h, --Socorro
Dê um breve resumo das opções e saia.

-dentro, --versão
Imprima a versão e saia.

Índice opções
O comportamento padrão é construir um índice, apenas para a saída HTML, em index.html.

--sem índice
Não produza o índice.

--multi-índice
Gere uma página para cada categoria e cada letra do índice, juntamente com um
página inicial index.html.

mesa of conteúdo opção
-toc, --índice
Insira um índice analítico. Para uma saída LATEX, ele insere um \ tableofcontents em
o início do documento. Para uma saída HTML, ele cria um índice analítico
em toc.html.

hiperlinks opções
--glob-de lima
Faça referências usando globalizações Coq do arquivo de arquivo. (Essas globalizações são
obtido com a opção Coq -dump-glob).

--não-externos
Não insira links para a biblioteca padrão Coq.

--externo url biblioteca
Defina a URL base para a biblioteca externa cujo prefixo raiz é libroot.

--coqlib url
Definir URL base para a biblioteca padrão Coq (o padrão é
http://coq.inria.fr/library/).

--coqlib_path dir
Defina o caminho base onde os arquivos Coq são instalados, especialmente os arquivos de estilo
coqdoc.sty e coqdoc.css.

-R dir coqdir
Mapeie o diretório físico dir para o diretório lógico Coq coqdir (semelhante à opção Coq
-R). Observação: a opção -R só tem efeito nos arquivos que a seguem no comando
linha, então você provavelmente precisará colocar esta opção primeiro.

Conteúdo opções
-g, --gallina
Não imprima provas.

-eu, --luz
Modo claro. Suprima as provas (como com -g) e os seguintes comandos:

* Definição de tática [recursiva]
* Dica / Dicas
* Requer
* Transparente / Opaco
* Argumento Implícito / Implícito
* Seção / Variável / Hipótese / Fim

O comportamento das opções -g e -l pode ser substituído localmente usando o (* begin show
*) ... (* end show *) ambiente (veja acima).

Língua opções
O comportamento padrão é assumir arquivos de entrada ASCII de 7 bits.

-latino1, --latin1
Selecione os arquivos de entrada ISO-8859-1. É equivalente a --inputenc latin1 --charset
iso-8859-1.

-utf8, --utf8
Selecione arquivos de entrada UTF-8 (Unicode). É equivalente a --inputenc utf8 --charset
utf-8. O suporte para LATEX UTF-8 pode ser encontrado em
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--inputenc corda
Fornece uma codificação de entrada LATEX, como uma opção para a entrada do pacote LATEX.

--charset corda
Especifique o conjunto de caracteres HTML, a ser inserido no cabeçalho HTML.

Use coqdoc online usando serviços onworks.net