Pacote: coq (8.9.0-1)

[ Fonte: coq  ]

proof assistant for higher-order logic (toplevel and compiler)

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

This package provides coqtop, a command line interface to Coq.

The proofgeneral package allows proofs to be edited using Emacs and XEmacs.

Etiquetas: Desenvolvimento de software: Compilador, Campo: Matemática, Implementado em: implemented-in::ocaml, interface::commandline, Interface de usuário(a): Interativo baseado em texto, Função: role::program, scope::utility, Kit de ferramentas de interface: Ncurses TUI

Outros pacotes relacionados a coq

• dep: coq-theories (= 8.9.0-1)

  assistente de provas para lógica de ordem superior (teorias)

• dep: libc6 (>= 2.28)

  GNU Biblioteca C: Bibliotecas compartilhadas
  também um pacote virtual fornecido por libc6-udeb

• dep: libcoq-ocaml-35sv0

  pacote virtual fornecido por libcoq-ocaml

• dep: ocaml-base-nox-4.05.0

  pacote virtual fornecido por ocaml-base-nox

• dep: ocaml-findlib

  management tool for OCaml libraries

• dep: ocaml-nox

  implementação do ML com um sistema de objetos baseado em classes (sem X)

• dep: python3

  interactive high-level object-oriented language (default python3 version)

• sug: coq-doc

  Pacote não disponível

• sug: ledit

  editor de linha para programas interativos

  ou readline-editor

  pacote virtual fornecido por ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: proofgeneral

  Pacote não disponível

• sug: why (>= 2.19)

  Pacote não disponível

Download de coq

Baixe para todas as arquiteturas disponíveis

Arquitetura	Tamanho do pacote	Tamanho instalado	Arquivos
i386	54,878.8 kB	208,963.0 kB	[lista de arquivos]