Using Coq


Topic Replies Activity
Metaprogramming in Coq? 2 July 20, 2019
What are the rules for shadowing Ltac2 tactics? 2 July 19, 2019
Rewriting by eta-equivalence 5 July 15, 2019
Failed definition: cannot ensure subtype 2 July 6, 2019
Blog post: Exponential blowup when using unbundled typeclasses to model algebraic hierarchies 15 July 4, 2019
Program Fixpoint consuming too much memory 4 June 29, 2019
How to force computation? 3 June 29, 2019
How to do deep embedding of propositional calculus? 2 June 24, 2019
Extensional setoids on functions, and rewriting 8 June 18, 2019
Safe mode checking nothing was admitted? 5 June 16, 2019
Newbie problem in CoqIDE on windows 3 June 13, 2019
Why Set < Top.i by default? 3 June 11, 2019
Decidable variable equality in Coq 4 June 11, 2019
Dependent pattern matching and specializing a function 3 June 6, 2019
Gallina function application in Ltac 2 June 5, 2019
How can I get types to compute? 3 May 30, 2019
Documentation of `{!Foo}? 26 May 29, 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
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