Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Yet Another Tactics Index for Beginners
4 answers
Mon 2024/04/15
[CUDW 2024] Coq User And Developers Workshop 2024 — July 1st - July 5th — Save the date!
Fri 2024/04/12
Iris 4.2 and std++ 1.10
Fri 2024/04/12
Replacing "true = false"
3 answers
Thu 2024/04/11
Ologs in Coq
Wed 2024/04/10
How to simplify single-branch match expressions?
2 answers
Mon 2024/04/08
Https://coq.inria.fr/opam/released is down
3 answers
Mon 2024/04/08
How to use binary floats in Flocq
3 answers
Fri 2024/04/05
How to proof a simple statement about rational numbers
4 answers
Tue 2024/03/26
Volunteers for ICFP 2024 Artifact Evaluation Committee (AEC)
Tue 2024/03/26
The Coq Club mailing list
IJCAR 2024: Call for Participation
Thu 2024/04/18
TYPES 2024: Call for Participation
Thu 2024/04/18
Formal Methods Teaching Workshop (FMTea 2024) Call for Papers
Thu 2024/04/18
[WiL] Women in Logic 2024 -- Final call for papers
Thu 2024/04/18
Regarding the performance of an extracted OCaml code from a Coq formalisation
3 replies
Wed 2024/04/17
Announcing VST 3.0beta
Tue 2024/04/16
LMW@LICS and ICALP '24 - Call for participation and scholarship applications
Tue 2024/04/16
VST 2.14 announcement
Tue 2024/04/16
Three Post-doc positions in RECIPROG project (located in France -- Lyon, Nantes and Paris)
Fri 2024/04/12
Coq User and Developer Workshop 2024
Fri 2024/04/12
Zulip
(
archive
)
Why is the fin type named `t`?
Find scope declaration
Specify flag on file?
Use disjunction with `match goal ` in Ltac
Graph2Tac downgrades Coq to 8.11
Opam package stdpp for 8.19
Building a toplevel
✔ Bug in Tactician
✔ Declaring that a property is hProp
Formally modeling systems
Proof Assistants Stack Exchange
Inductive from CoInductive?
Fri 2024/04/19
Proof for Question V.10
Thu 2024/04/18
Trouble proving a theorem using induction in Coq
Wed 2024/04/17
How do I enable this kind of rewriting?
1 answer
Tue 2024/04/16
Dealing an equality with coq. - beginner's question
1 answer
Mon 2024/04/15
Coq, Merging two forall definitions ranging over the same types
1 answer
Sun 2024/04/14
How to use a lemma that is defined in a Coq module?
1 answer
Fri 2024/04/12
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
1 answer
Thu 2024/04/11
How do I express a negative premise in Coq?
2 answers
Mon 2024/04/08
Coq - Are there functions which are provably equal but not definitionally equal?
Sun 2024/04/07
Stack Overflow
Inductive from CoInductive?
Thu 2024/04/18
Is is possible to rename a coq term?
1 answer
Sat 2024/04/13
What are the practical limitations of a non-turing complete language like Coq?
4 answers
Wed 2024/04/03
Coq : mutually recursive definitions with [mrec] in InteractionTrees Library
1 answer
Fri 2024/03/29
Is there a function that returns a list of values with specific type in OCaml?
2 answers
Thu 2024/03/28
Formualting a logic in farmer astronaught
3 answers
Mon 2024/03/25
How to prove (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)?
1 answer
Mon 2024/03/25
What's the correct setup for Kami (Coq framework for Bluespec) to be able to run on WSL Ubuntu?
1 answer
Fri 2024/03/22
Coq: keeping information in a match statement
2 answers
Fri 2024/03/22
Showing polynomial equality in coq/ssreflect
1 answer
Fri 2024/03/22
CS Theory Stack Exchange
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
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
Reddit
Classes in Coq
2 comments
Mon 2024/04/15
Defining Operational Semantics of Loops in Coq?
Sun 2024/04/07
Help: Constructing Theorem
6 comments
Sun 2024/03/17
The metacoq hymn
Thu 2024/02/15
Cant get syntax highlighting even after using vscoq. I have installed vscoq-language-server and coq-lsp through opam, installed their plugins in vscode. Also added the vscoqtop path in vscode. Still cant get the tactics highlighted.
2 comments
Wed 2024/01/31
Group Structure in Coq
2 comments
Thu 2024/01/25
Trying to figure out the following Lemma
12 comments
Wed 2024/01/24
The role of category theory in coq proofs
1 comment
Tue 2024/01/16
I don't know if this is the right place but I've been trying to use the VSCode extension to no avail
1 comment
Sun 2024/01/14
The ocamls defend the tower of functional programming against the attack of the generative llama ai
Wed 2024/01/10
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