Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
Surveying kernel vulnerabilities via non-proof term ways
Tue 2026/07/14
Stepping through a rocq script programatically?
1 answer
Fri 2026/07/10
Seventeenth Mathcomp sharing day
Wed 2026/07/08
Release of Rocq 9.3
Tue 2026/06/30
CFP - CPP 2027 - Certified Programs and Proofs
Mon 2026/06/29
2nd CFP: Tribute to Gilles Dowek workshop - July 18th, FLoC 26, Lisbon, Portugal
Wed 2026/06/24
Caching the entire Rocq package set with GitHub Actions
2 answers
Thu 2026/06/18
Why rewrite works one way with replace but both way with assert?
1 answer
Wed 2026/06/17
Problem with Ltac2 Notation and Control.enter
3 answers
Tue 2026/06/09
Blockchain formal verification @ category labs
Sat 2026/06/06
Zulip
Show unused lemmas in IDE
Surveying kernel vulnerabilities via non-proof term ways
✔ Confusing limitation (bug?) of `rewrite` tactic
HTML dependency graph
✔ Unset Guard Checking Prevented in Section
✔ vm_compute +/vs reflexivity
Extraction still prefixes things with "Coq_"?
Study buddies for Software Foundations volume 1
I have a dilemma, ROCQ or TLA+
Effect system for Rocq
Proof Assistants Stack Exchange
What is the best way to learn Iris completely independently
3 answers
Wed 2026/07/15
Coq - Overloading over multiple parameters with canonical structures
1 answer
Tue 2026/07/14
Mutual inductive proposition to define permutations with parity can't find decreasing argument of fix
2 answers
Tue 2026/07/14
Definition of choice types in mathcomp
1 answer
Fri 2026/07/10
Isar-style proofs for Rocq or Lean?
1 answer
Mon 2026/07/06
Why is this inductive definition considered "non-strictly positive"?
2 answers
Fri 2026/07/03
Construct the sum of reals indexing on a finType
1 answer
Wed 2026/06/24
What strategy should I learn to generalize my observations?
1 answer
Tue 2026/06/16
Transplanting rocq library files from one computer to another
2 answers
Thu 2026/06/11
About the use of command Canonical in Coq for mantaining Record Type information
1 answer
Sat 2026/06/06
CS Theory Stack Exchange
Is injectivity of constructors for (large) inductive types in Prop, such as squashing, consistent?
Mon 2026/04/27
Finite sets in Coq
1 answer
Fri 2025/01/31
Representations of Planar Graphs in Coq
2 answers
Wed 2025/01/08
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
Stack Overflow
Trouble with well-foundedness proofs
Sat 2026/07/11
How to get the fully qualified name of a Rocq tactic?
2 answers
Wed 2026/06/24
Is it possible to convert all higher-order logic and dependent type in Lean/Isabelle/Coq into first-order logic?
1 answer
Wed 2026/05/20
Which vector library to use in coq?
2 answers
Sun 2026/03/22
Can we prove equal subcases have equal induction hypotheses in recursion principle?
6 answers
Tue 2026/02/24
Coq (Rocq) standard library function for converting nat to string?
1 answer
Wed 2026/02/11
Equality of type with equal indices do not typecheck
3 answers
Wed 2026/01/28
How to prove manually (using calc) a Dafny lemma with an existential variable?
3 answers
Sun 2026/01/25
Kind of issue with two-steps recursion
2 answers
Fri 2026/01/09
How to scrutinize a `match` term with return type `a=b -> c`
1 answer
Mon 2025/10/20
