Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Possible lra bug
Sun 2023/03/26
[ANN] Bignums release 9.0.0
Mon 2023/03/20
Compute 121393+121393 causes stack overflow
8 answers
Sun 2023/03/19
Unexpectedly accepted eapply hypothesis
5 answers
Sun 2023/03/19
Coqtop Cannot Add File to Load Path
1 answer
Tue 2023/03/14
Is it possible to define a cbn-able universe cast with universe checking disabled?
9 answers
Wed 2023/03/08
Request for feedback: new convenience tactics/options for deterministic timouts & memory limits in Coq
Wed 2023/03/08
PhD position at Inria / Nantes Université (France)
Sat 2023/03/04
[CUDW 2023] Coq Users and Developers Workshop - June 26 to 30 - Save the Date!
2 answers
Thu 2023/03/02
Abstract and concrete access to a data structure
Wed 2023/02/22
The Coq Club mailing list
[Emacs] correct offsets in .glob files when unicode characters are present
Thu 2023/03/23
VerifyThis 2023: Call for Participation
Thu 2023/03/23
correct offsets in .glob files when unicode characters are present
3 replies
Thu 2023/03/23
[CMU-HoTT] Special lectures Directed Type Theory — via dependent profunctor-types following Kosta Dosen
Tue 2023/03/21
[ANN] Bignums release 9.0.0
Mon 2023/03/20
TABLEAUX 2023 - FIRST CALL FOR PAPERS
Sat 2023/03/18
ITP 2023: Call for Workshop and Tutorial Proposals
Thu 2023/03/16
Utrecht Summer School on Advanced Functional Programming 2023
Thu 2023/03/16
Call for Papers, Functional Software Architecture - FP in the Large
Thu 2023/03/16
LPAR 2023 Deadline extension
Tue 2023/03/14
Zulip
(
archive
)
Replacing a term in Dependent type without error
(deleted)
Proof with a subset type
4 color theorem preprint
use of tactic?
relation between numbers
Did INSTALLDEFAULTROOT stop working in 8.15?
use of destruct command
github.com/yannl35133/coq rewrite rule nonlinear n ++ n ==>n
Efficient raw input and output
Proof Assistants Stack Exchange
Rewrite with definitional equality and dependent types
3 answers
Thu 2023/03/23
I don't know how to fire up coqtail
1 answer
Tue 2023/03/21
How to reason about equality between different datatypes?
Mon 2023/03/20
How to abstract over function arity in Lean and Coq?
2 answers
Thu 2023/03/16
an argument why stack blocks are never unexpectedly freed in the RTL intermediate language in CompCert
1 answer
Wed 2023/03/15
How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument?
3 answers
Thu 2023/03/09
Coq Induction on Hypothesis destroys the Hypothesis
1 answer
Tue 2023/03/07
Destructing transitivity hypothesis on simple predicate logic
2 answers
Fri 2023/02/24
Program Fixpoint decreasing on measure produces unsolvable goal
1 answer
Thu 2023/02/23
How to get rid of opaque proof-terms in computation
2 answers
Sat 2023/02/18
Stack Overflow
How to scope Search to the current module only
1 answer
Sat 2023/03/25
What is a way to represent non-disjoint union in Coq?
2 answers
Sat 2023/03/25
__ in Ocaml extracted from Coq
1 answer
Sat 2023/03/25
'coqc' does not find findlib.conf
Sat 2023/03/25
How to proof recursively defined functions' prop in Coq
3 answers
Sat 2023/03/25
Coq returns cannot guess decreasing argument of fix. How to fix my function?
1 answer
Thu 2023/03/23
Decreasing argument (and what is a Program Fixpoint)
1 answer
Thu 2023/03/23
How to formally verify a compiler (frontend and/or backend)?
2 answers
Thu 2023/03/23
Why do these theorems of propositional logic allow for the same proof in Coq?
2 answers
Wed 2023/03/22
The apply rule in proof by cases
2 answers
Tue 2023/03/21
CS Theory Stack Exchange
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
3 answers
Thu 2023/03/23
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
Reddit
Software Foundations in Coq - Michael Ryan Clarkson
Sun 2023/03/26
Do we have a tutorial or a book which teaches coq without tactics, how to build proofs with lambdas in the CoC way?
8 comments
Thu 2023/03/23
Cannot Determine Decreasing Argument for Fix
19 comments
Thu 2023/03/09
How to prove theorems in coq in pure lambdas without tactic language?
8 comments
Fri 2023/03/03
Type Theory Forall #28 - Formally Verifying Smart Contracts using Coq, Pruvendo
Wed 2023/02/15
Is the set of free variables (FV) really a set or a list?
6 comments
Tue 2023/02/14
Why the set of type variables is infinite?
6 comments
Wed 2023/02/08
Companies using Coq / Formal Methods
10 comments
Thu 2023/01/26
Which areas of mathematics it is impossible to formalize in coq?
7 comments
Wed 2023/01/11
How do you introduce new numbers in a Proof?
1 comment
Sat 2022/12/31
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
