Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Windows installation from sources failure due to symbolic link
1 answer
Thu 2023/11/30
Modularizing Coq scripts with defining Parameters/proving Axioms
1 answer
Thu 2023/11/30
Internships at CNES, the French space agency
Mon 2023/11/27
[Very basic] stack overflow and computability
1 answer
Thu 2023/11/23
[ANN] coq-lsp 0.1.8
Tue 2023/11/14
Recursive definitions best practices
3 answers
Fri 2023/11/10
Call for volunteer maintainers of the Coq Library of Complexity Theory
Wed 2023/11/08
The Lemma body_push in Verif_stack of VC
Wed 2023/11/08
Formally verified endgame tablebase generator
Sun 2023/11/05
Implicit argument resolution
2 answers
Fri 2023/11/03
The Coq Club mailing list
Deadline extension for FICS Workshop (new deadline: 6/12/2023)
Fri 2023/12/01
fully qualified names in Print
Fri 2023/12/01
[TFP 2024 Final Call for Papers] 25th International Symposium on Trends in Functional Programming
Thu 2023/11/30
FLOPS 2024: final call for abstracts and papers
Thu 2023/11/30
2024 Alonzo Church Award Call for Nominations
Wed 2023/11/29
IJCAR 2024: 2nd call for co-located events
Mon 2023/11/27
'Call for Papers: 17th Conference on Intelligent Computer Mathematics (CICM 2024)
Fri 2023/11/24
Postdoc in Inria Gallinette team, Nantes -- Compositional Automated Verification for OCaml
Fri 2023/11/24
Third Call for Contributions - FICS Workshop (submission deadline: 1st December 2023)
Fri 2023/11/24
FMBC 2024 - First Call for Papers
Wed 2023/11/22
Zulip
(
archive
)
hol2dk, exporting HOL-Light proofs to Coq
Coq 8.18 slowdown
Lookup env with dependent types
`Program` and variable names
✔ Automatically generated names from `inversion` tactic.
Trouble installing Coq with opam
Q on installing from source on Ubuntu
Type deduction for Prop
✔ Problem installing HighSchoolGeometry on Ubuntu
Modularizing Coq Scripts with Defining Parameters
Proof Assistants Stack Exchange
Unfolding constants while rewriting using rewrite_strat and a hint database
Tue 2023/11/21
What is the best way to learn Iris completely independently
1 answer
Mon 2023/11/20
reference ospecialize and variable prim_base_irreducible not found in the current environment
Sun 2023/11/19
problem with unification
1 answer
Sat 2023/11/18
How to check a Zenon-generated proof with Coq?
Sat 2023/11/18
How to express that two equivalence relations can setoid rewrite across each other (Coq)
1 answer
Fri 2023/11/17
Induction COQ Question
1 answer
Mon 2023/11/13
Universe inconsistency errors when using ZF model in Coq
2 answers
Wed 2023/11/08
Why inductive types (or variants) are so rigid in terms of the set of constructors
1 answer
Wed 2023/11/01
Continue a section (with context) in coq
2 answers
Tue 2023/10/31
Stack Overflow
How to prove that nat_to_bin combines bin_to_nat b = normalize b in Coq
Fri 2023/12/01
How do I install a library in coq? (MacOS)
3 answers
Tue 2023/11/28
Is there a three-valued case analysis on patterns (a < b) (a = b) (a > b)?
2 answers
Tue 2023/11/28
How to prove an inequality
1 answer
Fri 2023/11/24
How can I give an alias to a type in coq
1 answer
Thu 2023/11/23
How to prove the goals in more elegant way using ssreflect?
2 answers
Thu 2023/11/23
Coq code in LaTeX using lstcoq does not work
1 answer
Mon 2023/11/20
How to continue case analysis of a nested match in coq?
1 answer
Sun 2023/11/12
Coq: Is there a way to define "map" for Ensemble
1 answer
Fri 2023/11/10
Why is `specialize` not an invalid tactic within a proof?
3 answers
Tue 2023/11/07
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
Can I always replace destruct with induction?
5 comments
Wed 2023/11/29
What does the WF notation in the coq documentation mean? Where do they define it?
2 comments
Mon 2023/11/27
Why the IndProp chapter is so hard and big???
8 comments
Tue 2023/11/21
Which IDE for coq is the best in 2023?
11 comments
Sun 2023/11/19
How to solve the trichotomy exercise from LF.IndProp.v (lt_ge_cases)
3 comments
Sat 2023/11/18
Formally verified tablebase generator
1 comment
Sun 2023/11/05
Help with total_maps
1 comment
Tue 2023/10/10
Syntax error: [induction_clause_list] expected after 'induction' (in [simple_tactic]).
3 comments
Thu 2023/10/05
Help with Inductive Relations
3 comments
Thu 2023/10/05
Help with Transitive Closure
2 comments
Tue 2023/10/03
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
