Balík: coq (8.12.0-3 a iné)

[ Zdroj: coq  ]

asistent dôkazov logiky vyššieho rádu (najvyššia úroveň a kompilátor)

Coq je asistent dôkazov logiky vyššieho rádu, ktorý umožňuje vývoj počítačových programov v súlade s ich formálnou špecifikáciou. Bol vyvinutý pomocou Objective Caml a Camlp5.

Tento balík poskytuje coqtop, rozhranie príkazového riadka ku Coq.

Grafické rozhranie ku Coq poskytuje balík coqide. Coq je tiež možné používať spolu s ProofGeneral, ktorý umožňuje upravovanie dôkazov pomocou emacs a xemacs. To vyžaduje, aby bol nainštalovaný balík proofgeneral.

Značky: Software Development: Kompilátor, Pole: Matematika, Implementované v: implemented-in::ocaml, interface::commandline, User Interface: Text-based Interactive, Role: role::program, scope::utility, Sada nástrojov používateľského rozhrania: Ncurses TUI

Ostatné balíky súvisiace s balíkom coq

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

  asistent dôkazov logiky vyššieho rádu (teórie)

• dep: libc6 (>= 2.29) [nie armel, mips64el, mipsel]

  knižnica GNU C - zdieľané knižnice
  tiež virtuálny balík poskytovaný balíkom libc6-udeb

• dep: libcoq-ocaml-1fwg6 [ppc64el]

  virtuálny balík poskytovaný balíkom libcoq-ocaml

• dep: libcoq-ocaml-4pem8 [arm64]

  virtuálny balík poskytovaný balíkom libcoq-ocaml

• dep: libcoq-ocaml-4s3g2 [armel, mips64el, mipsel]

  virtuálny balík poskytovaný balíkom libcoq-ocaml

• dep: libcoq-ocaml-otko2 [i386]

  virtuálny balík poskytovaný balíkom libcoq-ocaml

• dep: libcoq-ocaml-xs455 [amd64]

  virtuálny balík poskytovaný balíkom libcoq-ocaml

• dep: libcoq-ocaml-zuzr9 [armhf]

  virtuálny balík poskytovaný balíkom libcoq-ocaml

• dep: libnum-ocaml-3st20 [armel, mips64el, mipsel]

  virtuálny balík poskytovaný balíkom libnum-ocaml

• dep: libnum-ocaml-80ki3 [amd64, arm64, ppc64el]

  virtuálny balík poskytovaný balíkom libnum-ocaml

• dep: libnum-ocaml-hqq52 [armhf, i386]

  virtuálny balík poskytovaný balíkom libnum-ocaml

• dep: ocaml-base-nox-4.11.1

  virtuálny balík poskytovaný balíkom ocaml-base-nox

• dep: ocaml-findlib

  nástroj na správu knižníc OCaml

• dep: ocaml-nox

  implementácia ML s objektovým systémom založeným na triedach (bez podpory X)

• dep: python3

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

• sug: coq-doc

  Balík nie je dostupný

• sug: coqide

  asistent dôkazov logiky vyššieho rádu (rozhranie GTK)

  alebo proofgeneral

  generic frontend for proof assistants

• sug: ledit

  riadkový editor pre interaktívne programy

  alebo readline-editor

  virtuálny balík poskytovaný balíkom ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: why (>= 2.19)

  Balík nie je dostupný

Stiahnuť coq

Stiahnuť pre všetky dostupné architektúry

Architektúra	Verzia	Veľkosť balíka	Nainštalovaná veľkosť	Súbory
amd64	8.12.0-3+b3	88,333.2 kB	358,108.0 kB	[zoznam súborov]
arm64	8.12.0-3+b3	93,820.2 kB	384,451.0 kB	[zoznam súborov]
armel	8.12.0-3+b3	103,391.0 kB	412,954.0 kB	[zoznam súborov]
armhf	8.12.0-3+b3	86,284.5 kB	308,733.0 kB	[zoznam súborov]
i386	8.12.0-3+b3	85,826.4 kB	329,208.0 kB	[zoznam súborov]
mips64el	8.12.0-3+b3	103,385.3 kB	412,882.0 kB	[zoznam súborov]
mipsel	8.12.0-3+b3	103,402.0 kB	412,954.0 kB	[zoznam súborov]
ppc64el	8.12.0-3+b3	89,332.1 kB	371,137.0 kB	[zoznam súborov]