Package: coq (8.9.0-1)

[ Source: coq  ]

Bevisassistent for højere ordens logik - topniveau og kompiler

Coq er en bevisassistent for højere ordens logik, som tillader udviklingen af computerprogrammer som overholder deres formelle specifikationer. Det udvikles med brug af Objective Caml og Camlp5.

Denne pakke tilbyder coqtop, en kommandolinjegrænseflade til Coq.

Pakken proofgeneral gør at beviser kan redigeres via Emacs og XEmacs.

Tags: Software Development: Compiler, Field: Mathematics, Implemented in: implemented-in::ocaml, interface::commandline, User Interface: Text-based Interactive, Role: role::program, scope::utility, Interface Toolkit: Ncurses TUI

Other Packages Related to coq

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

  Bevisassistent for højere ordens logik - teorier

• dep: libc6 (>= 2.28)

  GNU C-bibliotek: Delte biblioteker
  also a virtual package provided by libc6-udeb

• dep: libcoq-ocaml-fl0a8

  virtual package provided by libcoq-ocaml

• dep: ocaml-base-nox-4.05.0

  virtual package provided by ocaml-base-nox

• dep: ocaml-findlib

  Håndteringsværktøj for OCaml-biblioteker

• dep: ocaml-nox

  ML implementering med et klasse-baseret object system (ingen X)

• dep: python3

  Interaktivt objektorienteret højniveausprog - standardversion af python3

• sug: coq-doc

  Package not available

• sug: ledit

  linjeredigeringsprogram for interaktive programmer

  or readline-editor

  virtual package provided by ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev

  Udviklingsbiblioteker og værktøjer for Coq

• sug: proofgeneral

  Package not available

• sug: why (>= 2.19)

  Package not available

Download coq

Download for all available architectures

Architecture	Package Size	Installed Size	Files
armhf	55,983.5 kB	197,337.0 kB	[list of files]