Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Redefining prod as a record?
Wed 2021/06/23
How to unset printing everything? (e.g. implicits, notations, etc)
1 answer
Wed 2021/06/23
Standard library of the future?
5 answers
Tue 2021/06/22
Need help to define CoFixpoint
1 answer
Mon 2021/06/21
[Call for Participation] July 2nd: The Coq Workshop 2021
Mon 2021/06/21
Coq to Why3: Proof of function correction
1 answer
Mon 2021/06/21
Coq to Why3: Proof of aux lemma of function correction
Sun 2021/06/20
Coq to Why3: with notation
1 answer
Fri 2021/06/18
Proof Ground 2021 - Call for Participation
Fri 2021/06/18
What is the syntax to give an explicit proof object (lambda term) to a lemma in Coq?
5 answers
Fri 2021/06/18
Zulip
Delayed execution of tactic
Reliable names from inductive definitions?
Stack overflow in Qed.
Problem in lemma writing
Two-sided queue
`false: bool` → contradiction — how?
What to do if Coq behaves differently on different machines?
TC failure inside Ltac `match`?
reading ssreflect related books
Automation and `mathcomp`.
Stack Overflow
How to apply/use buildin function
Thu 2021/06/24
Computational behaviour of Successor
2 answers
Wed 2021/06/23
(SOLVED - was a goal-printing bug) Coq - trivial induction on lists doesn't accept assumtion
Wed 2021/06/23
Proving two-list queue in coq
Wed 2021/06/23
Parametrizing a Module in Coq
1 answer
Tue 2021/06/22
Unifying types of identical meanings
1 answer
Tue 2021/06/22
Alternative tactic for `ssreflect`'s `move=>`
1 answer
Tue 2021/06/22
Implicit arguments propagation
1 answer
Tue 2021/06/22
proof of adding 1 to some number changes the parity in Coq
2 answers
Tue 2021/06/22
How to use symmetricity of an equality on Coq
2 answers
Tue 2021/06/22
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
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
This is My First Non-trivial Coq Development
3 comments
Wed 2021/05/19
Solving a mergesort sorting algorithm in Coq
5 comments
Tue 2021/05/18
Trivial problem with applying lemma.
2 comments
Mon 2021/05/17
How to make a function going from nat to decimal representation?
17 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
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
