Using Coq


Topic Replies Activity
About the Learning category 2 February 12, 2019
What do you think of axioms? 5 May 26, 2019
Machine learning and hammers for Coq 3 May 25, 2019
Documentation of `{!Foo}? 23 May 25, 2019
Understanding the Coq kernel 6 May 24, 2019
Fix followed by fun 5 May 24, 2019
Opaque vs Hint/Typeclasses Opaque 2 May 22, 2019
Equi-inhabitation of types predefined? 4 May 19, 2019
How to compose setoid_rewrite? 3 May 17, 2019
Blog post: Exponential blowup when using unbundled typeclasses to model algebraic hierarchies 9 May 16, 2019
How to detect (non)implicit arguments in ltac 7 May 7, 2019
Debugging Fixpoint execution 5 May 4, 2019
Equality between Types 2 May 4, 2019
Why3 3 May 2, 2019
Feature request: mode that disables Qed checking 6 May 2, 2019
Setoid rewrites with different types and implementations 3 April 14, 2019
Ltac Matching on evars and instantiation 3 April 11, 2019
Ltac that goes under binders to return a non constr value? 5 April 8, 2019
Unable to infer the type of placeholder in Record 4 April 7, 2019
Extensional setoids on functions, and rewriting 4 April 1, 2019
Typeclass inference and definition 2 March 30, 2019
Inductive proof automation 5 March 22, 2019
Equations, Elimination into Type 3 March 19, 2019
Equations, funelim and new variables 4 March 19, 2019
Documentation of Context? 4 March 16, 2019
Why Set < Top.i by default? 2 March 15, 2019
F_equal on records generating some kind of extensionality obligation? 5 March 13, 2019
How to learn Coq's module system? 2 March 12, 2019
Notation with binders *and* overall type annotation (like `fix`) 3 March 12, 2019
How to represent mathematical structures in Coq? 8 March 9, 2019