|
About the Learning category
|
|
1
|
334
|
February 12, 2019
|
|
Dependent Pair Injectivity equivalent to K
|
|
4
|
89
|
November 20, 2020
|
|
Smart Matches
|
|
3
|
89
|
November 12, 2020
|
|
Using CoqGym on my own files
|
|
1
|
65
|
October 29, 2020
|
|
Trying to prove sort algorithm correctness (for specific n), in search for hints
|
|
11
|
174
|
October 20, 2020
|
|
Bug in universe inference?
|
|
3
|
111
|
October 27, 2020
|
|
Stuck at Multiset.v contents_cons_inv
|
|
1
|
55
|
October 25, 2020
|
|
Why induction principle such as list_rect cannot be added in Hint database?
|
|
2
|
78
|
October 21, 2020
|
|
Tool for drawing coq project dependency graph?
|
|
15
|
378
|
October 14, 2020
|
|
Machine learning and hammers for Coq
|
|
21
|
1735
|
October 14, 2020
|
|
Inserting PPX annotations into extracted OCaml
|
|
2
|
110
|
October 12, 2020
|
|
Pattern matching: warn unused parameter?
|
|
1
|
67
|
October 10, 2020
|
|
What determines whether a custom entry is used for printing?
|
|
5
|
80
|
October 6, 2020
|
|
PHOAS encoding of pattern matching notations
|
|
6
|
102
|
October 5, 2020
|
|
Definitional equalities for universal properties?
|
|
2
|
73
|
October 4, 2020
|
|
How to utilize extensionality when rewriting
|
|
4
|
65
|
October 4, 2020
|
|
How can I use destruct given the constraint I have for index range of a list?
|
|
1
|
48
|
October 4, 2020
|
|
LL(n) notations in Coq
|
|
15
|
199
|
October 3, 2020
|
|
Another Proof From Logical Foundations Exercises
|
|
7
|
114
|
October 1, 2020
|
|
Article latex document class out of a Coq script
|
|
2
|
80
|
September 30, 2020
|
|
Corecursion via destructors?
|
|
2
|
84
|
September 27, 2020
|
|
[install] Notes on OCaml versions and Coq configuration
|
|
19
|
766
|
September 22, 2020
|
|
Software Foundations/ Verified Functional Algorithms Exercise
|
|
1
|
67
|
September 18, 2020
|
|
Coqchk
|
|
9
|
133
|
September 10, 2020
|
|
Preventing pollution of the instance context during Import
|
|
10
|
191
|
September 8, 2020
|
|
A template for organizing a Coq program verification project
|
|
0
|
115
|
September 5, 2020
|
|
Notation for inequality chain
|
|
4
|
241
|
August 24, 2020
|
|
Extended simply typed lyambda calculus substitution for let term
|
|
3
|
118
|
August 20, 2020
|
|
Not a valid ring equation
|
|
3
|
101
|
August 16, 2020
|
|
Why in silly_ex (the software foundation)the first hypothesis is useless
|
|
2
|
94
|
August 16, 2020
|
