Using Coq


Topic Replies Activity
About the Learning category 2 February 12, 2019
Coq on Windows using WSL 8 August 24, 2019
What is the canonical eliminator for Acc? Why uses Fix_F a nested match? 2 August 23, 2019
Shiftr and bound 5 August 23, 2019
A lemma about number catenating 4 August 18, 2019
How to learn Coq's module system? 3 August 18, 2019
Failed to do case analysis with dependent type and Program used 3 August 14, 2019
Using string_scope without Import-ing String 3 August 13, 2019
Use a submodule of OrderedType in FSets 5 August 11, 2019
What is the best way to proove a lemma with fixpoint definition? 7 August 6, 2019
Why does "Instance inst := ..." not parse? 3 August 5, 2019
A bit confused with notations 5 August 5, 2019
Why do I have to give match patterns which don't type check? 5 August 4, 2019
Survey of category theory in Coq 4 August 4, 2019
What do you think of axioms? 13 August 4, 2019
I cannot build Bignums 4 July 24, 2019
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