Using Coq


About the Learning category (2)
Inductive proof automation (5)
What do you think of axioms? (4)
Equations, Elimination into Type (3)
Equations, funelim and new variables (4)
Documentation of Context? (4)
Why Set < Top.i by default? (2)
F_equal on records generating some kind of extensionality obligation? (5)
Documentation of `{!Foo}? (18)
How to learn Coq's module system? (2)
Notation with binders *and* overall type annotation (like `fix`) (3)
How to represent mathematical structures in Coq? (8)
(Finite, discrete) Probabilities in Coq? (4)
Division and Mod by 0 (4)
Safe mode checking nothing was admitted? (2)
How much Coq do I need to know to learn SF Hoare Logic? (3)
How to uninstall Coq if it was installed from source? (2)
Trouble in implementing dependently typed lookup in Coq using Equations (3)
Debugging Fixpoint execution (4)
Proving properties for inductives with nested inductives (5)
Parametric Higher-order Abstract Syntax and Normalization by Evaluation (5)
Equations and FE (5)
Inequality between Types (9)