sci-mathematics/coq – Gentoo Packages

Version	amd64	x86	alpha	arm	arm64	hppa	mips	ppc	ppc64	riscv	sparc
9.0.0 : 0/9.0.0 T EAPI 8	~amd64	?x86	?alpha	?arm	~arm64	?hppa	?mips	?ppc	?ppc64	?riscv	?sparc
8.20.0-r1 : 0/8.20.0 T EAPI 8	amd64	~x86	?alpha	?arm	~arm64	?hppa	?mips	?ppc	?ppc64	?riscv	?sparc
8.19.2-r1 : 0/8.19.2 T EAPI 8	amd64	~x86	?alpha	?arm	~arm64	?hppa	?mips	?ppc	?ppc64	?riscv	?sparc
8.17.1-r1 : 0/8.17.1 T EAPI 8	~amd64	~x86	?alpha	?arm	~arm64	?hppa	?mips	?ppc	?ppc64	?riscv	?sparc

Other homepage(s)
https://github.com/coq/coq/
Upstream
Changelog https://github.com/coq/coq/releases/
Bugs-To https://github.com/coq/coq/issues/
Remote-Id https://github.com/coq/coq
Full description
Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: * the definition of functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to check these proofs by a small certification "kernel". Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories.
USE flags
Local Use Flags
- native-compiler
Global Use Flags
License
LGPL-2.1
Maintainer(s)
Gentoo Mathematics Project

Changelog	https://github.com/coq/coq/releases/
Bugs-To	https://github.com/coq/coq/issues/
Remote-Id	https://github.com/coq/coq