Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Showing falsity in a 'le' exercise from 'IndProp'
1 answer
Fri 2024/07/26
Verified Extraction for Coq 8.19
Tue 2024/07/23
ANN: docker-coq: Bump to Debian 12 (& opam 2.2.0)
Mon 2024/07/22
Tactic to fill a hypothesis of some term in the context
6 answers
Sat 2024/07/20
Coq Platform Docs: a documentation project for Coq and its Platform
Thu 2024/07/18
PhD opportunity: Coq Formalisation of Differentiable Logics
Sat 2024/07/13
[VsCoq] Release 2.1.4
Mon 2024/07/08
Nonstandard analysis in Coq
1 answer
Mon 2024/07/08
Why are then no clearly-visible signs of the Coq->Rocq rename?
4 answers
Fri 2024/07/05
Coq-Language-Server crashing multiple times
2 answers
Wed 2024/07/03
The Coq Club mailing list
Is it save to use (Proof Mode "Ltac2") in big projects?
1 reply
Sat 2024/07/27
Coq Platform Docs: a documentation project for Coq and its Platform
5 replies
Mon 2024/07/22
POPL 2025: Final Call for Workshops and Co-located Events (July 26 AOE)
Fri 2024/07/19
PhD position: Coq for AI
Fri 2024/07/12
CFP: CIFMA 2024 - Cognition and Formal Methods
Wed 2024/07/10
review of Kerjean's “Functorial Differential” at TLLA 2024 — [HoTT] Postdoc Category Theory
1 reply
Wed 2024/07/10
3rd Call for Papers: Mathematical User Interaction (MathUI'24)
Thu 2024/07/04
FSCD 2024: Free online participation, 10 - 13 July 2024
Wed 2024/07/03
IFL 2024: Second Call for Papers
Wed 2024/07/03
CFP - JFLA 2025 - Journées Francophones des Langages Applicatifs
Tue 2024/07/02
Zulip
(
archive
)
Stating theorem with depedent type
By what do you nest ?
inversion in ssreflect
Universe Polymorphism and eqn/destruct
✔ Error trying to compile coq-hott library
Trick: define Tactic Notations with multiple optional params
Call for bikeshedders
Defining an inductive and a function over it recursively
✔ Printing of notation in custom entry broken
Let coqc use files loadable in editor
Proof Assistants Stack Exchange
Coq - Overloading over multiple parameters with canonical structures
1 answer
Wed 2024/07/24
The uniform inheritance condition of coercions to dependent types in Coq
Wed 2024/07/24
Induction COQ Question
2 answers
Sat 2024/07/13
Code Review: $\mathbb{Z}[\sqrt{-2}]$ is an integral domain
2 answers
Sat 2024/07/06
Inconsistent failures of coercions when type checking in Coq
Fri 2024/07/05
Prove that a function's result cannot dependent on Prop-valued parameters in Coq
1 answer
Fri 2024/07/05
Uniqueness of proofs for inductively defined predicates
3 answers
Fri 2024/07/05
Is there a way to rename parameters when including/reusing a module type in Coq?
1 answer
Thu 2024/07/04
Found no matching subterm in goal while it does seem to be there when doing rewrite
Thu 2024/07/04
Type inference with type classes in Coq
2 answers
Thu 2024/07/04
Stack Overflow
Ltac matches applications of constructors of a type
Fri 2024/07/26
Try to understand SSReflect's "have" and square bracket
Thu 2024/07/25
Coq : transitivity fails on list intermediate term
Thu 2024/07/25
Need an inductive predicate over distinct pairs of list elements
Wed 2024/07/24
Install coq proof assistant from source - switch package not determined
1 answer
Thu 2024/07/18
Lightweight ways to prove an assembly language steps from a certain state to another state after variable number of instructions in Coq
2 answers
Wed 2024/07/17
How can I solve the "term type wrong" errror in coq?
Wed 2024/07/17
Tac to derive contradiction from circular equality (ie. smarter to discriminate)
1 answer
Fri 2024/06/28
How to make OCaml (or Coq) code from the llvmir code using vellvm framework
1 answer
Tue 2024/06/25
Coq repeating "destruct" for disjunctive hypothesis causing unwanted destruction in the end
3 answers
Tue 2024/06/25
CS Theory Stack Exchange
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
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
Reddit
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
How to Print and normalize the proof object?
4 comments
Tue 2024/07/16
Where is the source file where the "unfold" tactic is defined?
2 comments
Fri 2024/07/12
Best way to learn Ltac
3 comments
Fri 2024/07/12
Some problems encountered when switching from coqide to proof general
5 comments
Mon 2024/07/01
Coq, NixOS setup
Wed 2024/05/29
Required Formal Logic Books for Coq?
5 comments
Thu 2024/05/23
Required Functional Programming Experience Before Learning Coq?
24 comments
Sun 2024/05/19
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