Planet Coq

Link aggregator of discussions about the Coq interactive theorem prover

Discourse

How does one generate a static proof trees of a whole Coq Proof?
2 answers
Thu 2020/08/06
Can one translate from one ITP language to another automatically?
5 answers
Thu 2020/08/06
Can every theorem that has a proof be completed without DSL tactics?
6 answers
Thu 2020/08/06
Proving existence statements about coinductive types constructively
1 answer
Tue 2020/08/04
Notation for inequality chain
3 answers
Sat 2020/08/01
Applying hypothesis with unknown variables
1 answer
Fri 2020/07/31
术语：applicative functor
Fri 2020/07/31
Software Foundations/Logical Foundations Exercise
2 answers
Thu 2020/07/30
鉴于国内访问Coq中文论坛非常慢……
4 answers
Tue 2020/07/28
使用指南：通过电子邮件访问论坛
1 answer
Tue 2020/07/28

The Coq Club mailing list

Types in patterns
2 replies
Fri 2020/08/07
how to stop Coq from unfolding defined constants
2 replies
Thu 2020/08/06
"check_not_nested" error with Function
1 reply
Wed 2020/08/05
Access return values in theorem
4 replies
Wed 2020/08/05
apply iff_refl neither works or fails
2 replies
Tue 2020/08/04
[CfP] PADL 2021: Practical Aspects of Declarative Languages
Tue 2020/08/04
[CfP - Extended deadline] PLP-2020: The Seventh Workshop on Probabilistic Logic Programming
Mon 2020/08/03
Is there a measure for these functions?
7 replies
Mon 2020/08/03
smarter fold tactic
4 replies
Mon 2020/08/03
CMCS 2020: Call for Participation
Sun 2020/08/02

Stack Overflow

How to prove all proofs of le equal?
1 answer
Fri 2020/08/07
Instance of Ord typeclass for option
1 answer
Thu 2020/08/06
How to get the name of a named goal in the coq api
1 answer
Thu 2020/08/06
Greatest value in natural number list
1 answer
Wed 2020/08/05
How to get cardinal of ensembles explicitly
1 answer
Tue 2020/08/04
Coqtop cannot load file
2 answers
Mon 2020/08/03
Does using the unfold tactic followed by fold in Coq do anything?
2 answers
Sun 2020/08/02
How to instantiate hypotheses with variables that are out of scope
1 answer
Fri 2020/07/31
Using Notations in Records
1 answer
Thu 2020/07/30
IndProp: prove that Prop is not provable
5 answers
Thu 2020/07/30

CS Theory Stack Exchange

Applying hypothesis with unknown variables
1 answer
Sat 2020/08/01
An axiom for John Major's Equality
1 answer
Sat 2020/05/23
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
On the interpretation of coinduction in type theory
Mon 2019/12/23
Have the proofs in Buss's "On Goedel’s Theorems on Lengths of Proofs" been formalized (mechanically checked)?
Fri 2019/12/13
Proposition terms vs types in Coq
Mon 2019/12/02
Prove proof irrelevance in Coq?
1 answer
Mon 2019/08/26

Reddit

Custom Syntax, where to use it ?
1 comment
Mon 2020/08/03
Inductive Parameters for Module Types
6 comments
Wed 2020/07/29
Install proofweb
13 comments
Sat 2020/07/25
Is there an attempt to incorporate Cubical Type Theory into Coq?
1 comment
Sat 2020/07/11
Coq trick: (Almost) writing a function of type option α → α
Mon 2020/07/06
July 5-6: The Coq Workshop 2020
Tue 2020/06/30
Proofs and computation with trees
Sat 2020/06/20
Coq installation stuck at make?
5 comments
Thu 2020/06/18
Equations package: Termination proof is missing some precondition.
3 comments
Thu 2020/06/18
Why can't coq handle this replacement?
2 comments
Mon 2020/06/15

Coq News

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
Coq 8.11.0 is out
Tue 2020/01/28
Coq 8.11+beta1 is out
Fri 2019/12/06
Coq 8.10.2 is out
Fri 2019/11/29
Coq 8.10.1 is out
Fri 2019/10/25
Coq 8.10.0 is out
Mon 2019/10/07
Coq 8.10+beta3 is out
Mon 2019/09/16

Zulip