Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
[Job Offer] Production Engineer for the Coq Platform
Mon 2024/09/16
[VsCoq 2] Release 2.2.0
Sat 2024/09/14
Coq 8.20.0 is out
Wed 2024/09/11
Are dependent types necessary for modelling F Omega
Fri 2024/09/06
CoqMakefile.conf uses wrong name for coq_makefile command
Thu 2024/09/05
Beginner: Help understanding interaction between quantification and implication
9 answers
Mon 2024/09/02
Using arrows in coqtop
1 answer
Sun 2024/08/25
-beginner- recursive definition ill-formed
5 answers
Sat 2024/08/24
Big Specification workshop at the Newton Institute
Mon 2024/08/19
A Question on Defining Mutually Inductive Types with Universe Polymorphism
2 answers
Mon 2024/08/12
Zulip
(
archive
)
Decide boolean equality
Cannot infer instance in context which clearly contains it
Applying a "forall" hypothesis to a specific variable.
Decidable equality for nested inductives with EqDecision
Why does Fixpoint needs an argument ?
I can't understand the guard checker
✔ How to supply record parameters to record instance
Efficient graph datastructure in Coq
✔ negative unit type
Runtime of a program
Proof Assistants Stack Exchange
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
Induction COQ Question
2 answers
Mon 2024/08/12
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
1 answer
Fri 2024/08/09
Accessing nested typeclasses elegantly
1 answer
Fri 2024/08/09
Strict implicit arguments in Coq
1 answer
Thu 2024/08/08
How do I apply a lemma to both sides of an equality hypothesis?
2 answers
Tue 2024/08/06
Stack Overflow
Ltac for deterministic rewriting/sorting of operands
Sun 2024/09/15
How to define arg max in Coq
1 answer
Sat 2024/09/14
Casting a value from one fintype to another?
2 answers
Wed 2024/09/11
How can we use the familiar notation of integer arithmetics in ssreflect?
1 answer
Sun 2024/09/08
Stuck at a simple inequality of natural number proof in Coq
2 answers
Tue 2024/09/03
Coq - VSCode highlight Compute command in blue
1 answer
Tue 2024/09/03
Installing Coq on Mac Error – "“Coq-Platform~8.18~2023.11” is damaged and can’t be opened. You should eject the disk image."
Tue 2024/08/27
How does the CoqIDE Shortcuts panel work?
Tue 2024/08/27
Turn `P(?x)` into `exists x,P(x)` to give different instantiations for different subgoals in Coq
1 answer
Sun 2024/08/25
Why doesn't Coq notation defined by other notation working well?
1 answer
Sat 2024/08/24
CS Theory Stack Exchange
Finite sets in Coq
1 answer
Tue 2024/09/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
