Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Visualizing contributions to the Coq implementation and all Coq opam packages
3 answers
Fri 2021/05/14
Why Coq cannot compute the equality of two Real number (like R1,1,2,3) directly?
Wed 2021/05/12
Finding the right tactics to proof a theorem
1 answer
Mon 2021/05/10
Ltac2: Function to match a variable with a type
3 answers
Mon 2021/05/10
Equations 1.3 beta release
Thu 2021/05/06
如何解决模式匹配中类型的惰性求值
3 answers
Tue 2021/05/04
Should we need Coq on Android?
2 answers
Tue 2021/05/04
Dune is now required to build Coq
13 answers
Sun 2021/05/02
Formalized Divide-and-conquer for Lists
Fri 2021/04/30
Applying a tactic in depth-first manner
Mon 2021/04/19
Zulip
Helping unification for universe-like structure
Convert SSReflect `!=` to `<>`?
smooth manifolds in coq
unsigned integer library using Cyclic?
Proving properties of programs using the Specif sig type
bbv library: defining an alignment check
QuickChick - Not Checkable
Showing two types are equal inside theorem definition
Chaining a type-level and a term-level coercion
Universe for `pattern`
Stack Overflow
What does "eq^~" mean in Coq?
1 answer
Fri 2021/05/14
Coq extraction to Haskell
1 answer
Wed 2021/05/12
How to prove (~Q -> ~P) - > (P -> Q) in Coq
2 answers
Wed 2021/05/12
Compare sums ssreflect
1 answer
Sat 2021/05/08
Ssreflect probabilities (event and not event) sum to one
1 answer
Sat 2021/05/08
Rbar / Rbar_le / coquelicot lemma
1 answer
Sat 2021/05/08
less or equal relation with largest element of natural number list
3 answers
Tue 2021/05/04
What does `Control.refine` do in Ltac2?
1 answer
Mon 2021/05/03
Using a theorem on integer numbers for proving a theorem on natural numbers
1 answer
Sat 2021/05/01
Is it possible to prove oddb 0 = true?? coq
1 answer
Sat 2021/05/01
CS Theory Stack Exchange
Why does Coq have Prop?
4 answers
Fri 2021/04/09
Dependent eliminator for empty type in intensional Martin-Löf type theory
1 answer
Sun 2021/03/28
Defining inductive types in intensional type theory purely in terms of type-theoretic data
1 answer
Fri 2021/03/19
Impredicativity + large eliminations (with no excluded middle) in Coq
1 answer
Thu 2021/03/04
What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$?
Sat 2021/01/23
An axiom for John Major's Equality
Tue 2021/01/19
Defining finite sets inductively in a proof assistant?
1 answer
Tue 2020/05/05
Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?
2 answers
Fri 2020/03/13
Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook
1 answer
Thu 2020/03/05
Journals or conferences to submit formally verified libraries?
Wed 2020/02/12
Reddit
How to make a function going from nat to decimal representation?
16 comments
Fri 2021/05/14
Coq-club archives unavailable?
2 comments
Thu 2021/04/22
A small library for arity-generic datatype-generic programming in Coq
5 comments
Tue 2021/04/13
Please criticise my category theory code which (almost) gets to infinity categories
3 comments
Fri 2021/04/09
How are types in Coq more powerful than those of Haskell?
10 comments
Thu 2021/04/01
"Learning" real-analysis using Coq?
9 comments
Mon 2021/03/29
Naming conventions?
2 comments
Fri 2021/03/26
Trouble installing mathcomp
3 comments
Sat 2021/03/20
Proving 0 is a neutral element for addition using Coq
6 comments
Tue 2021/03/16
The Type Theory Forall Podcast #5 - The History of Coq'Art (Yves Bertot)
1 comment
Sun 2021/02/28
Coq News
Coq Platform 2021.02.0 is out
Fri 2021/02/26
Coq 8.13.1 is out
Mon 2021/02/22
Coq 8.13.0 is out
Thu 2021/01/07
Coq 8.12.2 is out
Fri 2020/12/11
Coq 8.13+beta1 is out
Mon 2020/12/07
Coq 8.12.1 is out
Mon 2020/11/16
Coq 8.12.0 is out
Mon 2020/07/27
Coq 8.12+beta1 is out
Wed 2020/06/17
Coq 8.11.2 is out
Tue 2020/06/09
Coq 8.11.1 is out
Fri 2020/04/24
