coq_8_14

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Name

coq

Main Program

coqtop

Programs

• coq-tex
• coq_makefile
• coqc
• coqc.byte
• coqchk
• coqdep
• coqdoc
• coqidetop.byte
• coqidetop.opt
• coqnative
• coqpp
• coqproofworker.opt
• coqqueryworker.opt
• coqtacticworker.opt
• coqtop
• coqtop.byte
• coqtop.opt
• coqwc
• coqworkmgr
• csdpcert
• ocamllibdep
• votour

Homepage

• https://coq.inria.fr

Version

8.14.1

License

• GNU Lesser General Public License v2.1

Maintainers

• Russell O'Connor
• Austin Seipp
• Vincent Laporte
• Théo Zimmermann

Platforms

• i686-cygwin
• x86_64-cygwin
• x86_64-darwin
• aarch64-darwin
• i686-freebsd
• x86_64-freebsd
• aarch64-freebsd
• x86_64-solaris
• aarch64-linux
• armv5tel-linux
• armv6l-linux
• armv7a-linux
• armv7l-linux
• i686-linux
• loongarch64-linux
• m68k-linux
• microblaze-linux
• microblazeel-linux
• mips-linux
• mips64-linux
• mips64el-linux
• mipsel-linux
• powerpc-linux
• powerpc64-linux
• powerpc64le-linux
• riscv32-linux
• riscv64-linux
• s390-linux
• s390x-linux
• x86_64-linux
• aarch64-netbsd
• armv6l-netbsd
• armv7a-netbsd
• armv7l-netbsd
• i686-netbsd
• m68k-netbsd
• mipsel-netbsd
• powerpc-netbsd
• riscv32-netbsd
• riscv64-netbsd
• x86_64-netbsd
• i686-openbsd
• x86_64-openbsd
• x86_64-redox

Defined

Source