Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
How to wrap bullets within a tactic?
2 answers
Tue 2024/10/08
Why do we need supplemental standard libraries?
7 answers
Mon 2024/10/07
Coq eats expression parentheses
8 answers
Fri 2024/10/04
Proofchat: A TCP client/server chat application written in Coq
10 answers
Thu 2024/10/03
[Postdoc position] Machine Learning for translation between formal mathematics libraries (2nd announcement)
Thu 2024/10/03
I want Guidance on Extending Coq for Custom Proof Automation
2 answers
Sat 2024/09/28
[VsCoq 2] Release 2.2.1
Tue 2024/09/24
[WITS 2025] Call for Contributions: 4th Workshop on the Implementation of Type Systems
Sun 2024/09/22
Extracting sequences from Coq to OCaml
1 answer
Sat 2024/09/21
Sixth Mathcomp sharing day
Wed 2024/09/18
The Coq Club mailing list
review of Max Zeuner defending “Constructive Algebraic Geometry”
1 reply
Mon 2024/10/07
POPL25: Call for Student Volunteers
Fri 2024/10/04
SEFM'24: Call for Participation
Thu 2024/10/03
Call for Participation: ANU Logic Summer School, Dec 2 -- 13, 2024
Thu 2024/10/03
Lectureship positions in Bath
Wed 2024/10/02
CADE-30 Call for Papers
Wed 2024/10/02
Call for Papers: FORMALISE 2025
Mon 2024/09/30
LICS 2025 Call for Papers and Call for Workshops
Fri 2024/09/27
Types post-proceedings call for papers
Thu 2024/09/26
Simulating lambda terms in lambda calculus
2 replies
Wed 2024/09/25
Zulip
(
archive
)
Difference between inaccessible indices and forced indices
Lemmas from Plus, Mult etc deprecated libraries
✔ WF rec and Below encoding - link ?
Setoid rewrite and regular equality
Why do tuples associate to the left?
`induction in` and `induction using`
Rewriting in a user-defined formula type
Unexpected warning about "incompatible prefix"
Pretty Printing Strings: line return
✔ Dual of Acc relation
Proof Assistants Stack Exchange
Ordinary substitution really corresponds to de Bruijn's substitution
1 answer
Thu 2024/10/03
Natural deduction in coq: implication introduction
1 answer
Thu 2024/10/03
Inconsistency Principle in Coq
3 answers
Sat 2024/09/21
Debug autorewrite in Coq
1 answer
Sat 2024/09/21
Deduction theorem in coq
1 answer
Fri 2024/09/20
How to use Modus Ponens in L axiomatic system
1 answer
Sun 2024/09/15
Is it possible to simplify/normalize nat arithmetic expressions in Coq?
1 answer
Tue 2024/09/10
Extensional sets in Coq and induction
1 answer
Fri 2024/09/06
Natural deduction with coq assistant prover
1 answer
Thu 2024/09/05
How does Coq guess `i` is decreasing?
1 answer
Tue 2024/09/03
Stack Overflow
How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))?
2 answers
Sat 2024/10/05
How to return the correct dependent type?
1 answer
Fri 2024/10/04
How to use the rewrite tactic in function arguments
1 answer
Tue 2024/10/01
Lemma cannot be used as a hint
2 answers
Tue 2024/09/24
Unfolding an opaque fixpoint in Coq
2 answers
Fri 2024/09/20
Proving non-linear equations and inequalities involving rational numbers in Coq
1 answer
Wed 2024/09/18
Ltac for deterministic rewriting/sorting of operands
1 answer
Wed 2024/09/18
Can I use a tactics under `coqtop -nois`?
1 answer
Wed 2024/09/18
What is to be used in place of exfalso omega?
1 answer
Tue 2024/09/17
How to define arg max in Coq
1 answer
Sat 2024/09/14
CS Theory Stack Exchange
Finite sets in Coq
1 answer
Thu 2024/10/03
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
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
Reddit
What are the dangers of using Hilbert's epsilon operator?
2 comments
Fri 2024/09/06
What is a good community for beginner questions?
3 comments
Fri 2024/09/06
Proof terms constructed by things like injection, tactic, etc
4 comments
Wed 2024/08/07
Reviews of "Programming Language Foundations" (Volume II of SF series)
6 comments
Mon 2024/08/05
subset-as-sigma-type VS subset-as-predicate
Fri 2024/08/02
"Theorems are types, and their proofs are programs that type-check at the corresponding type"?
7 comments
Fri 2024/08/02
Trudging through Software Foundations Vol 1 / Formal Verification Research
8 comments
Sun 2024/07/28
How to autogenerate a hypothesis name (H1) in "assert (H1 := term)" in Ltac2?
2 comments
Fri 2024/07/26
How does a cumputer understand Fixpoint?
5 comments
Tue 2024/07/23
How to replace ("pose proof") with ("refine" + "let ... in")
7 comments
Mon 2024/07/22
