Link aggregator of discussions about the
interactive theorem prover
Windows installation from sources failure due to symbolic link
Modularizing Coq scripts with defining Parameters/proving Axioms
Internships at CNES, the French space agency
[Very basic] stack overflow and computability
[ANN] coq-lsp 0.1.8
Recursive definitions best practices
Call for volunteer maintainers of the Coq Library of Complexity Theory
The Lemma body_push in Verif_stack of VC
Formally verified endgame tablebase generator
Implicit argument resolution
The Coq Club mailing list
Deadline extension for FICS Workshop (new deadline: 6/12/2023)
fully qualified names in Print
[TFP 2024 Final Call for Papers] 25th International Symposium on Trends in Functional Programming
FLOPS 2024: final call for abstracts and papers
2024 Alonzo Church Award Call for Nominations
IJCAR 2024: 2nd call for co-located events
'Call for Papers: 17th Conference on Intelligent Computer Mathematics (CICM 2024)
Postdoc in Inria Gallinette team, Nantes -- Compositional Automated Verification for OCaml
Third Call for Contributions - FICS Workshop (submission deadline: 1st December 2023)
FMBC 2024 - First Call for Papers
hol2dk, exporting HOL-Light proofs to Coq
Coq 8.18 slowdown
Lookup env with dependent types
`Program` and variable names
✔ Automatically generated names from `inversion` tactic.
Trouble installing Coq with opam
Q on installing from source on Ubuntu
Type deduction for Prop
✔ Problem installing HighSchoolGeometry on Ubuntu
Modularizing Coq Scripts with Defining Parameters
Proof Assistants Stack Exchange
Unfolding constants while rewriting using rewrite_strat and a hint database
What is the best way to learn Iris completely independently
reference ospecialize and variable prim_base_irreducible not found in the current environment
problem with unification
How to check a Zenon-generated proof with Coq?
How to express that two equivalence relations can setoid rewrite across each other (Coq)
Induction COQ Question
Universe inconsistency errors when using ZF model in Coq
Why inductive types (or variants) are so rigid in terms of the set of constructors
Continue a section (with context) in coq
How to prove that nat_to_bin combines bin_to_nat b = normalize b in Coq
How do I install a library in coq? (MacOS)
Is there a three-valued case analysis on patterns (a < b) (a = b) (a > b)?
How to prove an inequality
How can I give an alias to a type in coq
How to prove the goals in more elegant way using ssreflect?
Coq code in LaTeX using lstcoq does not work
How to continue case analysis of a nested match in coq?
Coq: Is there a way to define "map" for Ensemble
Why is `specialize` not an invalid tactic within a proof?
CS Theory Stack Exchange
Formalization of matching logic (logic behind K Framework)
Can I define nested mutually dependent types in Coq?
Defining finite sets inductively in a proof assistant?
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?
Can I always replace destruct with induction?
What does the WF notation in the coq documentation mean? Where do they define it?
Why the IndProp chapter is so hard and big???
Which IDE for coq is the best in 2023?
How to solve the trichotomy exercise from LF.IndProp.v (lt_ge_cases)
Formally verified tablebase generator
Help with total_maps
Syntax error: [induction_clause_list] expected after 'induction' (in [simple_tactic]).
Help with Inductive Relations
Help with Transitive Closure
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