Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Is there a way to redirect Coqide messages and errors to the same output?
1 answer
Thu 2023/02/02
MathComp 1.16.0 released
Thu 2023/02/02
Stuck on destructing
2 answers
Tue 2023/01/17
Volunteer co-maintainer needed for Docker-Coq
Tue 2023/01/17
Coq Platform 2022.09.1 release with Coq 8.16.1
Tue 2023/01/17
VsCoq 0.3.7 is out
Wed 2023/01/11
Verification Jobs @ Cryspen (France/Germany)
Wed 2023/01/11
Need coq tutor
1 answer
Tue 2023/01/10
How do I write a summation on Coq?
2 answers
Mon 2023/01/09
Coq LSP release 0.1.2
1 answer
Mon 2023/01/09
The Coq Club mailing list
Functions and equations
5 replies
Sat 2023/02/04
Job offer — [CfP] CT2023 workshop on implementing Dosen's categorial programming
Fri 2023/02/03
Postdoc position on design and/or verification of distributed systems at the University of Birmingham
Thu 2023/02/02
MathComp 1.16.0 released
Thu 2023/02/02
RAMiCS 2023 - Call for participation
Thu 2023/02/02
FSCD 2023: Extended deadline (Abstract: February 4/ Submission: February 9)
Wed 2023/02/01
ETAPS 2023 Call For Participation
Mon 2023/01/30
Call for Papers: DaLí - Special Issue of the J. of Logical and Algebraic Methods in Programming
Mon 2023/01/30
Stuck with weird goal imposed by Fix_eq
4 replies
Mon 2023/01/30
[ANN] coq-lsp release 0.1.4
Sun 2023/01/29
Zulip
(
archive
)
efficient way
alternate way of writing
Convincing Coq accept my definition
list of points
Coq 8.17 is *fast*
existence
list nat
✔ One final lemma
execute example
How to write incremental modular coq code
Proof Assistants Stack Exchange
How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument?
3 answers
Fri 2023/02/03
What is the idiomatic way in Coq to write recursive functions over product types?
1 answer
Thu 2023/02/02
Destruction of bound dependent types
1 answer
Tue 2023/01/31
What exactly is setoid hell?
3 answers
Thu 2023/01/26
In Coq, is there a simpler tactic for introducing a disjunction and immediately destructing it?
3 answers
Wed 2023/01/25
Coq simpl failing to do beta reduction in this fixpoint expression
1 answer
Sat 2023/01/21
Are there any ergonomic ways to deal with finite types in Coq?
3 answers
Fri 2023/01/20
Subsequences in Coq
2 answers
Fri 2023/01/13
How to write a summation in Coq
1 answer
Thu 2023/01/12
How do I define a function in Coq with if...then..else behavior?
2 answers
Sun 2023/01/08
Stack Overflow
Another question about how to make Coq accept a Fixpoint definition
1 answer
Fri 2023/02/03
Is there a way to redirect Coqide messages and errors to the same output?
1 answer
Tue 2023/01/31
"Cannot instantiate metavariable P of type ..." when destructing in Coq proof mode
1 answer
Mon 2023/01/30
Forcing evaluation of terms before extraction, or other ways to test extracted functions?
1 answer
Sat 2023/01/28
Is it possible to make Coq accept a class of Fixpoint functions if we provide proofs of argument size reduction?
2 answers
Sat 2023/01/28
Beta expansion in coq: can I make a term into a function, abstracting over another given term?
2 answers
Thu 2023/01/26
In Coq, why is `nat` a `Type`, even though it's actually a `Set`?
2 answers
Wed 2023/01/25
What does InjL and InjR operator means in coq-Iris?
1 answer
Tue 2023/01/24
Understanding \is a unit in ssreflect
2 answers
Tue 2023/01/24
using addf_div for rat_numDomainType
1 answer
Mon 2023/01/23
CS Theory Stack Exchange
Why does Coq have Prop?
4 answers
Fri 2022/12/09
What exactly is "large elimination"?
2 answers
Tue 2022/11/15
A Coq question : How to prove the image of the two same valued variables under a function are same?
1 answer
Sun 2022/07/10
Defining functions on non-inductive types using LEM in Coq
1 answer
Fri 2022/01/21
Prove proof irrelevance in Coq?
1 answer
Fri 2021/10/29
How does axiom K contradict univalence?
2 answers
Sun 2021/09/26
Does the order of declarations in an inductive type matter?
3 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
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
Reddit
Companies using Coq / Formal Methods
10 comments
Thu 2023/01/26
Which areas of mathematics it is impossible to formalize in coq?
6 comments
Wed 2023/01/11
How do you introduce new numbers in a Proof?
1 comment
Sat 2022/12/31
Has anyone attempted to solve the first 3 Tao Analysis I chapters in coq?
4 comments
Mon 2022/12/05
Boolean Short Circuiting
7 comments
Wed 2022/11/30
Coq vs SMTs
1 comment
Sat 2022/11/19
A Type-Based Approach to Divide-And-Conquer Recursion in Coq [pdf]
4 comments
Thu 2022/11/10
prove DeMorgan law in coq
5 comments
Wed 2022/10/19
How I feel doing software foundations
2 comments
Sat 2022/09/10
Autocompletion in Vim.
6 comments
Mon 2022/09/05
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
