Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Release of the Coq platform 2021.02.1 - Coq 8.13.2
Tue 2021/04/13
Certified Elm web apps
Mon 2021/04/12
Apparently bad installation of coq (im a newbie)
4 answers
Sun 2021/04/11
Renaming Coq
Thu 2021/04/08
Our code of conduct might be incomplete
Fri 2021/04/02
Proof Ground 2021 - Call for Problems
Fri 2021/04/02
Not an inductive product
5 answers
Wed 2021/03/31
Building Coq with Bazel - need help with plugins
5 answers
Wed 2021/03/31
Nix package for coq theories with dependencies
2 answers
Wed 2021/03/31
Rtauto slower than tauto
Mon 2021/03/29
Zulip
Tricky nia goals
Possible polynomial NP-complete solution
How to prove that geom. series (with q < 1) goes to 0
Tail-call optimization in reduction machines
Weird typeclass behavior
How to Debug slow QED?
Can't simplify goal...
overlapping notations in different scopes
A better type ascription syntax `foo : bar`
Real numbers sum <= sum Unable to unify error
Stack Overflow
Implement Boruvka's algorithm in Coq
2 answers
Tue 2021/04/13
Cauchy-Schwartz Inequality in Coq?
2 answers
Sat 2021/04/10
"Symbol's value as variable is void" when adding a path to coqtop when opening emacs
1 answer
Sat 2021/04/10
FoldR using FoldL on finite lists
1 answer
Fri 2021/04/09
coq auto says simple apply fails but it works manually
1 answer
Fri 2021/04/09
Coq infotheo Unable to Unify error when comparing sums of reals
Fri 2021/04/09
Dependent-type design when the parameters indicate the result should not exist
1 answer
Thu 2021/04/08
Tower of powersets
1 answer
Thu 2021/04/08
How to prove n <= n + S m in coq?
2 answers
Thu 2021/04/08
Coq infotheo %B is_true
2 answers
Wed 2021/04/07
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
1 answer
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
A small library for arity-generic datatype-generic programming in Coq
3 comments
Tue 2021/04/13
Please criticise my category theory code which (almost) gets to infinity categories
1 comment
Fri 2021/04/09
How are types in Coq more powerful than those of Haskell?
4 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
A formal proof of safegcd bounds
Sun 2021/02/21
Simple untyped lambda calculus interpreter
1 comment
Sat 2021/02/13
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
