Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Allowing large elimination
3 answers
Tue 2024/10/22
Assistance Getting Rid of Superfluous Universe levels?
3 answers
Mon 2024/10/21
Is there a public roadmap for the Rocq rename?
3 answers
Fri 2024/10/11
How to wrap bullets within a tactic?
6 answers
Tue 2024/10/08
Coq eats expression parentheses
10 answers
Tue 2024/10/08
Why do we need supplemental standard libraries?
7 answers
Mon 2024/10/07
Proofchat: A TCP client/server chat application written in Coq
10 answers
Thu 2024/10/03
[Postdoc position] Machine Learning for translation between formal mathematics libraries (2nd announcement)
Thu 2024/10/03
I want Guidance on Extending Coq for Custom Proof Automation
2 answers
Sat 2024/09/28
[VsCoq 2] Release 2.2.1
Tue 2024/09/24
The Coq Club mailing list
PriSC @ POPL'25: 2nd Call for Paper
Mon 2024/10/21
FSCD 2025: Call for Workshop Proposals
Mon 2024/10/21
FSCD 2025: First Call for Papers
Fri 2024/10/18
POPL 2025 Call for Tutorials (deadline extended: Oct 25th, 2024)
Thu 2024/10/17
[TFP 2025 2nd Call for Papers] 25th International Symposium on Trends in Functional Programming (Oxford, UK)
Fri 2024/10/11
1st CfP: SLE 2025 - 18th ACM SIGPLAN International Conference on Software Language Engineering
Thu 2024/10/10
Dafny Workshop at POPL 2025 (deadline extension)
Wed 2024/10/09
PhD and postdoc position at the University of Copenhagen
Wed 2024/10/09
Assistant Professor (Tenure Track) position at ETH Zurich
Wed 2024/10/09
review of Max Zeuner defending “Constructive Algebraic Geometry”
1 reply
Mon 2024/10/07
Zulip
(
archive
)
✔ Pretty printing library
proving `not (Type equiv Prop)` from hurkens
Disable coqdoc unicode pretty-printing
Surprising failure to infer typeclasses
How to find input breaking test?
About and Scope fail in 8.20
Implicit argument in records
Runtime of a program
Help: Tuto about combining tactics
✔ Dual of Acc relation
Proof Assistants Stack Exchange
I need help with min problem
Tue 2024/10/22
How does Coq guess `i` is decreasing?
2 answers
Tue 2024/10/22
Skolem functions in COQ
2 answers
Mon 2024/10/21
Principle like UIP on Types with Decidable Equality but for Inequality Proofs
1 answer
Sun 2024/10/20
How does the case (destruct) tactic change the goal?
1 answer
Wed 2024/10/16
About the use of command Canonical in Coq for mantaining Record Type information
1 answer
Mon 2024/10/14
How can I generate equalities from an application in Coq?
1 answer
Sat 2024/10/12
Natural deduction in coq: implication introduction
1 answer
Thu 2024/10/03
Inconsistency Principle in Coq
3 answers
Sat 2024/09/21
Debug autorewrite in Coq
1 answer
Sat 2024/09/21
Stack Overflow
How to prove existence in COQ?
1 answer
Tue 2024/10/15
How to prove if a list `n::l` is an in-order merge of 2 lists `n::l1` `l2`, then `l` is an in-order merge of `l1` and `l2` in Coq?
Wed 2024/10/09
How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))?
2 answers
Sat 2024/10/05
How to return the correct dependent type?
1 answer
Fri 2024/10/04
How to use the rewrite tactic in function arguments
1 answer
Tue 2024/10/01
Lemma cannot be used as a hint
2 answers
Tue 2024/09/24
Unfolding an opaque fixpoint in Coq
2 answers
Fri 2024/09/20
Proving non-linear equations and inequalities involving rational numbers in Coq
1 answer
Wed 2024/09/18
Ltac for deterministic rewriting/sorting of operands
1 answer
Wed 2024/09/18
Can I use a tactics under `coqtop -nois`?
1 answer
Wed 2024/09/18
CS Theory Stack Exchange
Finite sets in Coq
1 answer
Thu 2024/10/03
Simple Coq simplification question
1 answer
Fri 2024/06/07
What should a proof of correctness for a typechecker actually be proving?
3 answers
Thu 2024/06/06
Formalization of matching logic (logic behind K Framework)
3 answers
Wed 2023/08/16
Notation problem
1 answer
Thu 2023/06/01
Can I define nested mutually dependent types in Coq?
1 answer
Sat 2023/05/13
Defining finite sets inductively in a proof assistant?
1 answer
Tue 2023/04/25
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
Reddit
What are the dangers of using Hilbert's epsilon operator?
2 comments
Fri 2024/09/06
What is a good community for beginner questions?
3 comments
Fri 2024/09/06
Proof terms constructed by things like injection, tactic, etc
4 comments
Wed 2024/08/07
Reviews of "Programming Language Foundations" (Volume II of SF series)
6 comments
Mon 2024/08/05
subset-as-sigma-type VS subset-as-predicate
Fri 2024/08/02
"Theorems are types, and their proofs are programs that type-check at the corresponding type"?
7 comments
Fri 2024/08/02
Trudging through Software Foundations Vol 1 / Formal Verification Research
8 comments
Sun 2024/07/28
How to autogenerate a hypothesis name (H1) in "assert (H1 := term)" in Ltac2?
2 comments
Fri 2024/07/26
How does a cumputer understand Fixpoint?
5 comments
Tue 2024/07/23
How to replace ("pose proof") with ("refine" + "let ... in")
7 comments
Mon 2024/07/22