Package: coq (8.12.0-3 and others) [debports]

[ Source:  ]

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.

En grafisk grænseflade for Coq tilbydes i pakken coqide. Coq kan også bruges med ProofGeneral, som tillader at beviser redigeres med emacs og xemacs. Dette kræver at pakken proofgeneral er installeret.

Other Packages Related to coq

• dep: coq-theories (= 8.12.0-3+b3)

  Bevisassistent for højere ordens logik - teorier

• dep: libcoq-ocaml-4s3g2

  virtual package provided by libcoq-ocaml

• dep: libnum-ocaml-3st20

  virtual package provided by libnum-ocaml

• dep: ocaml-base-nox-4.11.1

  Package not available

• dep: ocaml-findlib

  Håndteringsværktøj for OCaml-biblioteker

• dep: ocaml-nox

  Overgangspakke for OCaml

• dep: python3

  Interaktivt objektorienteret højniveausprog - standardversion af Python 3

• sug: coq-doc

  documentation for Coq

• sug: coqide

  bevisassistent for højere ordens logik (gtk-brugerflade)

  or proofgeneral

  Generisk brugerflade for bevisassistenter

• 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: why (>= 2.19)

  Package not available

Download coq

Download for all available architectures

Architecture	Version	Package Size	Installed Size	Files
alpha (unofficial port)	8.12.0-3+b3	103,380.6 kB	412,882.0 kB	[list of files]