Using Coq


Topic Replies Activity
About the Learning category 2 February 12, 2019
What is the correct way to port to v8.10 after deprecation of Z notations? 4 October 17, 2019
Axiomatic ZFC 7 October 16, 2019
Unfolding identifiers applied to specific values only 5 October 16, 2019
Confusing sentence in Mike Nahas's tutorial 2 October 16, 2019
Machine learning and hammers for Coq 11 October 14, 2019
Poll: coding style - constructor parameters 4 October 11, 2019
Coq on Windows using WSL 35 October 11, 2019
Replace hypothesis with implication without adding its premise as subgoal 2 October 7, 2019
Instance resolution: restricting the introduction of evars 3 October 1, 2019
Are there developments of model theory in Coq? 1 October 1, 2019
If my purpose of using Coq is purely mathematical, what are the most suitable resources can I learn Coq from? 2 September 30, 2019
« if _ is _ then _ else » notation 2 September 21, 2019
Case of two ‘fix’es 2 September 19, 2019
Memory limit for commands 1 August 27, 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