Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
A logo that Rocqs
Wed 2024/12/11
AI for Math Fund
Thu 2024/12/05
Preview of Ltac2 Visual Debugger is now available
Mon 2024/12/02
MathComp 2.3.0 released
Thu 2024/11/28
Eighth Mathcomp sharing day
Tue 2024/11/26
Lean Together 2025
Mon 2024/11/25
Unfold tactic not helpful
2 answers
Mon 2024/11/25
Lecturer/Senior Lecturer in Mathematically Structured Programming at Strathclyde
Fri 2024/11/22
Rocq Sharing Analyser (new plugin to print debug info)
Tue 2024/11/05
Release of Iris 3.4 and std++ 1.11
Thu 2024/10/31
The Coq Club mailing list
[CPP'25] Call for Participation: Certified Programs and Proofs (CPP) 2025
Wed 2024/12/11
TYPES 2025: First Call for Contributions
Tue 2024/12/10
FSCD 2025: Second Call for Papers
Tue 2024/12/10
Announcement and CfP, Conference on Intelligent Computer Mathematics (CICM), 6-11 october 2025, Brasilia, Brazil
Mon 2024/12/09
JFLA 2025 - Inscriptions ouvertes
Thu 2024/12/05
Paid internship position at Virginia Tech, USA
Wed 2024/12/04
PhD positions at Nottingham
Tue 2024/12/03
(Post-)Doctoral Positions at Chapman U
Mon 2024/12/02
MathComp 2.3.0 released
Thu 2024/11/28
CfP: DisCoTec 2025
Wed 2024/11/27
Zulip
(
archive
)
Avoiding divergence of typeclass search
✔ Add hints for lia
Setoid's Type class search doesn't simplify fixpoint?
SF: weird comment about record
How should induction work
Universe polymorphism for built-in types
Links Section and Generalizable Variables
✔ Ltac Unfold only in matched context?
Ltac: applying tactic to all hypotheis
How to reuse computed Typeclass instances?
Proof Assistants Stack Exchange
An optimal proof of the theorem in Coq
1 answer
Thu 2024/12/12
Proving a disjunction without left nor right in Coq
1 answer
Wed 2024/12/11
Error when making CoqProject
2 answers
Wed 2024/12/11
Induction COQ Question
2 answers
Tue 2024/12/10
Coq: how to apply "only once"
2 answers
Tue 2024/12/10
Coq: unfold a class nested in the goal
1 answer
Mon 2024/12/09
Coq: when to give a context variable of imported package as argument
1 answer
Sun 2024/12/08
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
1 answer
Sun 2024/12/08
No notations from custom entries inside the proof state
1 answer
Sat 2024/12/07
How to automate resolving circular dependencies between definitions and obligations in Coq?
1 answer
Sat 2024/12/07
Stack Overflow
Coq Error Syntax error: '.' expected after [gallina] (in [vernac_aux])
1 answer
Thu 2024/12/12
Coq & Emacs: Cannot compile Coq - No such file or directory
1 answer
Thu 2024/12/12
Dependent Pair Types
1 answer
Wed 2024/12/11
Cannot rewrite in goal using Equations Package in Coq?
1 answer
Wed 2024/12/11
I'm having difficulty definining a property in Coq, not sure how to approach
2 answers
Wed 2024/12/11
how to prove 2 step induction of list in coq using fix tactic
Mon 2024/12/09
Coq is reusing a term in Induction Hypothesis, instead of creating a fresh one
1 answer
Mon 2024/12/09
How to prove theorems about mutual inductive types by using tactics in Coq?
2 answers
Sun 2024/12/08
What does "Some" mean in coq?
1 answer
Tue 2024/12/03
Efficient Record Construction in Coq: Is Direct Proof Inclusion Possible?
3 answers
Thu 2024/11/28
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
(Coq based) Verified Matching of Regular Expressions with Lookarounds
2 comments
Thu 2024/12/05
Type Theory Forall #46 - Realizability Models, BHK Interpretation, Dialectica - Pierre-Marie Pédrot
Fri 2024/11/29
#45 What is Type Theory and What Properties we Should Care About - Pierre-Marrie Pédrot
Mon 2024/11/25
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
