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. Typical

applications include the certification of properties of programming languages,

the formalization of mathematics and teaching.

Here are 429 public repositories matching this topic...

coq / coq

Star 3k

Open

[wish] attribute #[primitive]

gares commented Oct 7, 2020

In math comp we are considering switching some records to primitive, but the current syntax for that is very ugly, see
math-comp/math-comp#591
since one has to Set/Unset before/after each record declaration.

Read more

good first issue kind: feature part: attributes

Open

The source code of Coq’s extraction plugin is using a lot of physical equalities

11

Open

Int63 numbers are not captured by patterns in proofs

2

Find more good first issues →

UniMath / UniMath

Star 658

Open

pi_1(circle, pt) = Z

1

benediktahrens commented May 20, 2019

There is now a type circle in UniMath.SyntheticHomotopyTheory.Circle2. It would be great to define pi_1 of a pointed type, and to show that pi_1(circle, pt) \simeq Z.

Read more

good first issue

Open

Unify names of builder functions

5

Open

Upstream code on foundations and categories from UniMath/TypeTheory

2

Find more good first issues →

QuickChick / QuickChick

Star 173

Randomized Property-Based Testing Plugin for Coq

testing coq

• Updated Sep 10, 2020
• Coq

Created by Gérard Pierre Huet, Thierry Coquand

Released 1989

Latest release 3 months ago

Repository

coq/coq

Website

coq.inria.fr

Wikipedia

Wikipedia