Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
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
Annals of Formalized Mathematics
Fri 2024/03/22
How to automatically extract anonymous subterms in a goal
Tue 2024/03/19
MetaCoq 1.3.1 release
Tue 2024/03/19
Coq Plugin to output hypotheses, goal and tactic in JSON
2 answers
Tue 2024/03/12
Coq 8.19.1
Mon 2024/03/04
Ltac with variadic argument
1 answer
Mon 2024/03/04
[Question; very basic] Stack-based virtual machine test
2 answers
Fri 2024/03/01
[RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages
2 answers
Thu 2024/02/29
The Coq Club mailing list
CICM 2024 - Extended deadline - Call for Papers
Thu 2024/03/28
LSFA 2024: CALL FOR PAPERS
Wed 2024/03/27
Extended Deadline April 8, 2024 (abstracts April 1, 2024): 17th Conference on Intelligent Computer Mathematics (CICM 2024)
Tue 2024/03/26
ISR 2024: Call for Participation
Tue 2024/03/26
TyDe 2024: First call for papers and extended abstracts
Mon 2024/03/25
Volunteers for ICFP 2024 Artifact Evaluation Committee (AEC)
Mon 2024/03/25
Annals of Formalized Mathematics
Fri 2024/03/22
FME Teaching Tutorial on March 28, 2024, 3 pm CET: Prof Wolfram Kahl, McMaster University, Canada: Teaching with CalcCheck
Fri 2024/03/22
[PPDP'2024 CfP] The 26th International Symposium on Principles and Practice of Declarative Programming Call for Papers
Wed 2024/03/20
Funded PhD Position in Formalizing/Verification of Golang (Application Deadline 2024-03-31)
Wed 2024/03/20
Zulip
(
archive
)
Defining Fixpoint with new Relation on Sequences
Specify flag on file?
Coq Docker image for M2 mac architecture
Open Goal View
✔ Curly brace in ssreflect
Extraction Singleton for specific types
Opam package stdpp for 8.19
Packaging a Coq library for nix?
Performance of arbitrary length integer computations in Coq
Info from match clauses, and destruct difficulties
Proof Assistants Stack Exchange
Tactic to Propify a bool expression
1 answer
Thu 2024/03/28
Coq - Overloading over multiple parameters with canonical structures
1 answer
Tue 2024/03/26
Coq: Language server crashes when trying to introduce an equality-hypothesis
Tue 2024/03/26
Creating a tactic for 'destructing' a list by last element?
2 answers
Tue 2024/03/26
Why does the following Coq code fail to meet Coq's positivity requirement for inductive types?
Fri 2024/03/22
Assistance using destruct on an equality proof for functors
1 answer
Fri 2024/03/22
How to prove non-existence of terms that contain themselves in Coq
4 answers
Thu 2024/03/21
For formal proofs of graph structures and algorithms, which proof assistant should I learn?
3 answers
Mon 2024/03/18
In Coq, what tactic can I use to remove a True precondition from a hypothesis
2 answers
Mon 2024/03/18
Proving non-existence of "least" subtype generator in Coq
1 answer
Fri 2024/03/15
Stack Overflow
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
Syntax of the case tactic in coq
1 answer
Fri 2024/03/22
Understanding nat_ind2 in Logical Foundations
1 answer
Tue 2024/03/19
Why assuming singleton elimination and definitional proof irrelevance leads to UIP, in Coq?
Tue 2024/03/19
Split multiple conjuncts in the goal
2 answers
Thu 2024/03/14
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
Help: Constructing Theorem
6 comments
Sun 2024/03/17
The metacoq hymn
1 comment
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
Trying to prove 1/1 is in lowest terms
5 comments
Wed 2024/01/03
Do we have pen-and-paper exercises for CIC?
2 comments
Sun 2023/12/24
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