Planet Coq

Link aggregator of discussions about the Coq interactive theorem prover

Discourse

Overload list notation
1 answer
Sat 2021/09/25
Dune + proof general
3 answers
Thu 2021/09/23
Why the tactic "apply... with..." cannot be applied to hypotheses?
8 answers
Thu 2021/09/23
[ANN] PyCoq preview release
Thu 2021/09/23
Can the Equations plugin generate a graph that does not reference the original function?
1 answer
Wed 2021/09/22
An awkward inductive definition that resists `destruct`
1 answer
Mon 2021/09/20
How to define the SEP(R) clauses?
Mon 2021/09/20
Awkwardness with coinductive universes
2 answers
Fri 2021/09/17
How to use tactic forward_if Q?
4 answers
Thu 2021/09/16
School on Univalent Mathematics, Cortona (Italy), July 17-23, 2022
Wed 2021/09/15

The Coq Club mailing list

Compiler verification homeworks
3 replies
Fri 2021/09/24
RE: Substitution of sub-tree occurrence in a tree
Fri 2021/09/24
Substitution of sub-tree occurrence in a tree
3 replies
Fri 2021/09/24
Reminder: 2 year position on HoTT and related topics in Stockholm, deadline Friday next week
Fri 2021/09/24
[ANNOUNCE] pyCoq initial release
1 reply
Thu 2021/09/23
Using SerAPI in a plugin
7 replies
Wed 2021/09/22
Termination for three argument addition function on natural numbers
6 replies
Wed 2021/09/22
PEPM 2022 - Second Call for Papers
Wed 2021/09/22
Call for Tutorials and Workshops: PLDI 2022
Tue 2021/09/21
unexpected lia failure
3 replies
Mon 2021/09/20

Zulip

Stack Overflow

How to generalize a variable on both sides of an equation in Coq?
1 answer
Sat 2021/09/25
Avoid duplicating code for applying tactics in both hypothesis and goal
Fri 2021/09/24
Error: Cannot interpret this number as a value of type nat
1 answer
Mon 2021/09/20
Software Foundations Volume 1: Tactics: injection_ex3
1 answer
Mon 2021/09/20
Trying to define a "rect2"-like function on heterogeneous vectors
1 answer
Mon 2021/09/20
erewrite that asks for hypothesis first?
1 answer
Mon 2021/09/20
Is it possible to turn unification errors into goals in Coq?
1 answer
Fri 2021/09/17
ssreflect inversion, I need two equations instead of one
2 answers
Thu 2021/09/16
VSCoq ProofView not printing
Thu 2021/09/16
Binary tree inversion in Coq
1 answer
Wed 2021/09/15

CS Theory Stack Exchange

Does the order of declarations in an inductive type matter?
3 answers
Sat 2021/09/25
How does axiom K contradict univalence?
2 answers
Sat 2021/09/25
How would I go about learning the underlying theory of the Coq proof assistant?
4 answers
Wed 2021/08/18
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

Reddit

Formal verification manager job at Google - Coq experience a plus
Thu 2021/09/23
New to Coq: How to compile .vo files and run command line?
2 comments
Sun 2021/09/05
Slides & Videos of the Coq Workshop 2021
Mon 2021/08/30
Is Coq’ Art book still worth it?
6 comments
Wed 2021/08/11
Clashing versions of ocaml on cpdt text compile
4 comments
Tue 2021/08/10
Join together types
2 comments
Fri 2021/08/06
Simple Example of Inductive
5 comments
Tue 2021/06/22
Proving a function body of an Abstract Data Type
3 comments
Mon 2021/05/31
Proving that [insert] produces a Binary Search Tree
5 comments
Sat 2021/05/22
Silveroak - Formal specification and verification of hardware
Thu 2021/05/20

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