Link aggregator of discussions about the
interactive theorem prover
Possible lra bug
[ANN] Bignums release 9.0.0
Compute 121393+121393 causes stack overflow
Unexpectedly accepted eapply hypothesis
Coqtop Cannot Add File to Load Path
Is it possible to define a cbn-able universe cast with universe checking disabled?
Request for feedback: new convenience tactics/options for deterministic timouts & memory limits in Coq
PhD position at Inria / Nantes Université (France)
[CUDW 2023] Coq Users and Developers Workshop - June 26 to 30 - Save the Date!
Abstract and concrete access to a data structure
The Coq Club mailing list
[Emacs] correct offsets in .glob files when unicode characters are present
VerifyThis 2023: Call for Participation
correct offsets in .glob files when unicode characters are present
[CMU-HoTT] Special lectures Directed Type Theory — via dependent profunctor-types following Kosta Dosen
[ANN] Bignums release 9.0.0
TABLEAUX 2023 - FIRST CALL FOR PAPERS
ITP 2023: Call for Workshop and Tutorial Proposals
Utrecht Summer School on Advanced Functional Programming 2023
Call for Papers, Functional Software Architecture - FP in the Large
LPAR 2023 Deadline extension
Replacing a term in Dependent type without error
Proof with a subset type
4 color theorem preprint
use of tactic?
relation between numbers
Did INSTALLDEFAULTROOT stop working in 8.15?
use of destruct command
github.com/yannl35133/coq rewrite rule nonlinear n ++ n ==>n
Efficient raw input and output
Proof Assistants Stack Exchange
Rewrite with definitional equality and dependent types
I don't know how to fire up coqtail
How to reason about equality between different datatypes?
How to abstract over function arity in Lean and Coq?
an argument why stack blocks are never unexpectedly freed in the RTL intermediate language in CompCert
How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument?
Coq Induction on Hypothesis destroys the Hypothesis
Destructing transitivity hypothesis on simple predicate logic
Program Fixpoint decreasing on measure produces unsolvable goal
How to get rid of opaque proof-terms in computation
How to scope Search to the current module only
What is a way to represent non-disjoint union in Coq?
__ in Ocaml extracted from Coq
'coqc' does not find findlib.conf
How to proof recursively defined functions' prop in Coq
Coq returns cannot guess decreasing argument of fix. How to fix my function?
Decreasing argument (and what is a Program Fixpoint)
How to formally verify a compiler (frontend and/or backend)?
Why do these theorems of propositional logic allow for the same proof in Coq?
The apply rule in proof by cases
CS Theory Stack Exchange
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
Why does Coq have Prop?
What exactly is "large elimination"?
A Coq question : How to prove the image of the two same valued variables under a function are same?
Defining functions on non-inductive types using LEM in Coq
Prove proof irrelevance in Coq?
How does axiom K contradict univalence?
Does the order of declarations in an inductive type matter?
How would I go about learning the underlying theory of the Coq proof assistant?
Dependent eliminator for empty type in intensional Martin-Löf type theory
Software Foundations in Coq - Michael Ryan Clarkson
Do we have a tutorial or a book which teaches coq without tactics, how to build proofs with lambdas in the CoC way?
Cannot Determine Decreasing Argument for Fix
How to prove theorems in coq in pure lambdas without tactic language?
Type Theory Forall #28 - Formally Verifying Smart Contracts using Coq, Pruvendo
Is the set of free variables (FV) really a set or a list?
Why the set of type variables is infinite?
Companies using Coq / Formal Methods
Which areas of mathematics it is impossible to formalize in coq?
How do you introduce new numbers in a Proof?
Coq Platform 2021.02.0 is out
Coq 8.13.1 is out
Coq 8.13.0 is out
Coq 8.12.2 is out
Coq 8.13+beta1 is out
Coq 8.12.1 is out
Coq 8.12.0 is out
Coq 8.12+beta1 is out
Coq 8.11.2 is out
Coq 8.11.1 is out