Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Typeclasses on functions
1 answer
Thu 2022/09/29
Can I achieve some specific project with Coq?
3 answers
Wed 2022/09/28
Volunteer interim maintainers needed for VsCoq
Tue 2022/09/27
Generating latex from coq theorems (Coq to Latex)
1 answer
Mon 2022/09/26
What is unsafe about the Ltac2.Constr.Unsafe module?
2 answers
Fri 2022/09/23
CFP - JFLA 2023 - Journées Francophones des Langages Applicatifs
Wed 2022/09/14
Best way to express that a type is inhabited in a way that allows getting the habitant
1 answer
Tue 2022/09/13
Divmod equation
3 answers
Sun 2022/09/11
Defining functions in proof mode
6 answers
Fri 2022/09/09
Coq 8.16.0 has been tagged
Mon 2022/09/05
The Coq Club mailing list
POPL 2023 Call for Tutorials
Sat 2022/10/01
Call for Presentations: PriSC 2023 @ POPL 2023
Sat 2022/10/01
Fully funded PhD positions in logic, semantics of programs and verification at University of Sheffield, UK (Deadline: 18.10.2022)
Thu 2022/09/29
FME Teaching Tutorials series continues on September 30, 2022, at 3 pm CEST: Prof Michael Leuschel (Heinrich-Heine-University Düsseldorf, Germany) on "Teaching Formal Methods and Theoretical Computer Science with ProB"
Fri 2022/09/23
PLMW@POPL 2023: Call For Scholarship Applications (DEADLINE: 10/14 AoE)
Fri 2022/09/23
RAMiCS 2023 - Deadline extension
Fri 2022/09/23
CoqPL 2023: Call for Presentations
Wed 2022/09/21
PLDI 2023 First Call for Papers
Wed 2022/09/21
[TFP 2023 Call for Papers] 24th International Symposium on Trends in Functional Programming
Mon 2022/09/19
CFP - JFLA 2023 - Journées Francophones des Langages Applicatifs
Wed 2022/09/14
Zulip
(
archive
)
Using Streams.Exists
✔ IDE support for Dune
✔ Printing of primitive floats
✔ Find term of a given type
Code typechecks in Coq 8.13, but not in 8.14
SF lecture videos
✔ New project
Extracting to a directory
✔ coqtop is not running
✔ Lost in Tactic Notation
Proof Assistants Stack Exchange
Coq Typeclass on Functions Gets Confused by Equality
Tue 2022/09/27
.CoqMakefile.d required by CoqMakefile but not generated
Thu 2022/09/15
If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq?
Fri 2022/09/02
Can I unfold not all things but only one thing in Coq?
1 answer
Thu 2022/09/01
Has anyone accidentally "proven" a false theorem using what was later found to be a critical bug?
3 answers
Wed 2022/08/31
How can I correspond a hypothesis to a decidable axiom in match (in Coq)?
1 answer
Wed 2022/08/31
How do I prove this property in Coq?
1 answer
Tue 2022/08/30
How can I use a (three terms) decidable axiom in a case analysis?
1 answer
Tue 2022/08/30
Natural deduction with coq assistant prover
1 answer
Sat 2022/08/27
How can I search only all of the lemmas in a different module (in Coq)?
1 answer
Thu 2022/08/25
Stack Overflow
Using VST with GCC
1 answer
Fri 2022/09/30
Install why3-coq on MacBook Pro
Thu 2022/09/29
Can someone help me with this proof about the pumping lemma using coq?
Mon 2022/09/19
How do I exit coqtop REPL?
2 answers
Sun 2022/09/18
Overloading operators in Coq via typeclasses and notation scopes: Is there anything special about the '+' and '*' symbols?
1 answer
Fri 2022/09/09
How to call proof asistant Coq from external software
2 answers
Thu 2022/09/08
setoid_rewrite failed with MathClasses Coq
1 answer
Thu 2022/09/08
How does one automatically make a `COQ_PROJ.opam` install script automatically from a Coq Project/Package?
Wed 2022/09/07
I'm trying to build a proof in Coq that two different permutation definitions are equivalent, but the non-inductive side is not working
1 answer
Thu 2022/09/01
Prove equality with eq_rect without UIP
1 answer
Mon 2022/08/22
CS Theory Stack Exchange
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
How does axiom K contradict univalence?
2 answers
Sun 2021/09/26
Does the order of declarations in an inductive type matter?
3 answers
Sat 2021/09/25
How would I go about learning the underlying theory of the Coq proof assistant?
4 answers
Wed 2021/08/18
Why does Coq have Prop?
4 answers
Fri 2021/04/09
Dependent eliminator for empty type in intensional Martin-Löf type theory
1 answer
Sun 2021/03/28
Defining inductive types in intensional type theory purely in terms of type-theoretic data
1 answer
Fri 2021/03/19
Impredicativity + large eliminations (with no excluded middle) in Coq
1 answer
Thu 2021/03/04
Reddit
How I feel doing software foundations
2 comments
Sat 2022/09/10
Autocompletion in Vim.
5 comments
Mon 2022/09/05
Breaking Badfny
Fri 2022/09/02
How does one access the dependent type unification algorithm from Coq's internals -- especially the one from apply and the substitution solution?
1 comment
Fri 2022/07/15
Type Theory Forall Podcast - Experience Report Learning Coq
Sat 2022/06/04
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
4 comments
Mon 2022/05/30
The reference info was not found in the current environment.
2 comments
Thu 2022/05/19
Coq make failing on Omega
2 comments
Thu 2022/05/19
Type Theory Forall Episode #17 The Lost Elegance of Computation - Conal Elliott
Tue 2022/05/10
Hey, at risk of making a tired question, I could use a little help with something that I'm finding myself stuck on as an of-two-days proof assistant and Coq user. ∀x : ℕ, 3 | (x + 5x). Specifically, what's got me is showing that ∀x y z : ℕ, (z|x and z|y) -> z|(x + y). Attempt in post body.
8 comments
Mon 2022/05/09
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
