Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
Postdoc position at TU Delft
1 answer
Tue 2026/10/06
NWPT 2026: Deadline Extension Until October 10th
Tue 2026/10/06
JFLA2027 : Dernier appel à communications
Tue 2026/10/06
Research roles at Melbourne on seL4, agentic security, neural theorem proving
Mon 2026/10/05
Rocq 9.3.0
3 answers
Fri 2026/10/02
Using vsrocq language server with Emacs
1 answer
Tue 2026/09/29
Research positions on Isabelle verification of Agentic seL4
Tue 2026/09/29
TYPES 2026: Post-proceedings Call for Papers
Wed 2026/09/23
NWPT 2026, Final Call for Contributions
Tue 2026/09/15
RocqPL 2027 Call for Presentations
Wed 2026/09/09
Zulip
Installation error of Rocq 9.3.0 (macOS)
✔ Why can't `injection` handle partially applied construc...
Status of SProp
Under the hood of Search
syntax for abstract tactic block
Ocaml recommended version
Implicits in class constraints
Rocq termination checking
Complexity Theory
Recursively defined theorem with some measure
Proof Assistants Stack Exchange
Is there a way to make Rocq's "if-then-else" accept setoid rewriting?
Tue 2026/10/06
In Rocq, can I unfold a single "let _ := _ in _" at a time?
1 answer
Sun 2026/09/27
Is `rat` harder to use than `Q` for rational numbers in Rocq?
1 answer
Tue 2026/09/22
Debug autorewrite in Coq
1 answer
Fri 2026/09/11
Make [...] explicit in Rocq/vsRocq
1 answer
Wed 2026/09/02
Non-typed dependent pattern matching in Rocq
1 answer
Thu 2026/08/20
An upgrade from Mathcomp v2.4.0 to v2.5.0 going wrong with rationals
1 answer
Sat 2026/08/15
Error when making CoqProject
2 answers
Mon 2026/08/03
Is there a model that contradicts `@eq Type t1 t2 -> @eq Prop t1 t2` or can it be proven?
1 answer
Sun 2026/08/02
Induction COQ Question
2 answers
Sun 2026/08/02
CS Theory Stack Exchange
Coq proof - no verifier can be simultaneously sound and complete on a µ-sensitive claim from an identical classical trace. Check me please!
Thu 2026/09/10
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
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
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
How to deal with potentially-aliased arguments in VST?
1 answer
Sat 2025/09/13
