|
About the Learning category
|
|
1
|
662
|
February 12, 2019
|
|
Using Add Relation for Setoid equivalence of rationals
|
|
0
|
52
|
April 26, 2022
|
|
One weird trick to encode modal types
|
|
0
|
52
|
April 25, 2022
|
|
How to import Basics.v in Induction.v of LF using VS Coq extension
|
|
6
|
112
|
April 14, 2022
|
|
DFA In COQ
|
|
5
|
75
|
April 13, 2022
|
|
Machine learning and hammers for Coq
|
|
36
|
3407
|
April 7, 2022
|
|
Functional induction with remember
|
|
2
|
106
|
April 1, 2022
|
|
Completely confused by a trivial SSR proof with case
|
|
3
|
86
|
March 30, 2022
|
|
Annoying warnings when Requiring/Importing ssreflect
|
|
4
|
68
|
March 28, 2022
|
|
Inductive proof automation
|
|
6
|
525
|
March 25, 2022
|
|
What is a hammer/atp within the logic of coq that does things like induction in coq?
|
|
1
|
69
|
March 24, 2022
|
|
How to state mutual/nested lemmas
|
|
8
|
170
|
March 22, 2022
|
|
Saerch in VSCoq
|
|
5
|
74
|
March 22, 2022
|
|
Stdlib documentation online?
|
|
1
|
65
|
March 20, 2022
|
|
More informative response to stucked proofs?
|
|
3
|
101
|
March 18, 2022
|
|
Indeterminate value for partial functions trick
|
|
4
|
163
|
March 14, 2022
|
|
Stream of non-empty lists to stream
|
|
2
|
94
|
March 11, 2022
|
|
How to have vscode find coq?
|
|
3
|
214
|
March 10, 2022
|
|
Verify a intrusive linked list is memory safe with Coq
|
|
4
|
132
|
March 7, 2022
|
|
How to activate the messages window in vscode like the coqide has?
|
|
1
|
99
|
March 5, 2022
|
|
Help with notations that "look alike"
|
|
2
|
91
|
March 4, 2022
|
|
Coqtop not found
|
|
10
|
1859
|
March 3, 2022
|
|
How to create a Powerset of MSetList?
|
|
2
|
106
|
February 24, 2022
|
|
How to use coqc's `verbose` option?
|
|
0
|
69
|
February 23, 2022
|
|
How to install Coq when it says the repository cannot be found? (e.g. issues with m1 chip mac, apple)
|
|
21
|
353
|
February 17, 2022
|
|
Applying a theorem that doesn't match exactly
|
|
4
|
126
|
February 6, 2022
|
|
How to assume an identifier bound to a type with decidable equality using Coq.Structures.Equalities?
|
|
2
|
144
|
January 29, 2022
|
|
Ill-formed recursive definition using `let fix`
|
|
2
|
140
|
January 25, 2022
|
|
Building a project with coq_makefile, using a library specified in .coqrc
|
|
0
|
102
|
January 25, 2022
|
|
Prooving the length of a list under constraint
|
|
8
|
230
|
January 25, 2022
|