|
Coq on Windows using WSL
|
36
|
November 5, 2019
|
|
Blog post: Exponential blowup when using unbundled typeclasses to model algebraic hierarchies
|
16
|
November 4, 2019
|
|
Best practices for machine-level representation of numbers and bitwise operations
|
7
|
October 31, 2019
|
|
Does flambda slow down Coq?
|
9
|
October 28, 2019
|
|
What is the correct way to port to v8.10 after deprecation of Z notations?
|
8
|
October 24, 2019
|
|
Check if a previously-stated theorem proves a particular subgoal?
|
3
|
October 23, 2019
|
|
Machine learning and hammers for Coq
|
15
|
October 23, 2019
|
|
Deriving instances for Haskell extracted data-types
|
4
|
October 19, 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
|
|
Poll: coding style - constructor parameters
|
4
|
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
|
|
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
|
