|
Machine learning and hammers for Coq
|
|
45
|
3922
|
June 6, 2022
|
|
Induction hypothesis vs. termination checker
|
|
2
|
97
|
June 5, 2022
|
|
Using Add Relation for Setoid equivalence of rationals
|
|
0
|
125
|
April 26, 2022
|
|
One weird trick to encode modal types
|
|
0
|
116
|
April 25, 2022
|
|
How to import Basics.v in Induction.v of LF using VS Coq extension
|
|
6
|
391
|
April 14, 2022
|
|
DFA In COQ
|
|
5
|
160
|
April 13, 2022
|
|
Functional induction with remember
|
|
2
|
187
|
April 1, 2022
|
|
Completely confused by a trivial SSR proof with case
|
|
3
|
144
|
March 30, 2022
|
|
Annoying warnings when Requiring/Importing ssreflect
|
|
4
|
128
|
March 28, 2022
|
|
Inductive proof automation
|
|
6
|
586
|
March 25, 2022
|
|
What is a hammer/atp within the logic of coq that does things like induction in coq?
|
|
1
|
127
|
March 24, 2022
|
|
How to state mutual/nested lemmas
|
|
8
|
291
|
March 22, 2022
|
|
Saerch in VSCoq
|
|
5
|
157
|
March 22, 2022
|
|
Stdlib documentation online?
|
|
1
|
106
|
March 20, 2022
|
|
More informative response to stucked proofs?
|
|
3
|
166
|
March 18, 2022
|
|
Indeterminate value for partial functions trick
|
|
4
|
248
|
March 14, 2022
|
|
Stream of non-empty lists to stream
|
|
2
|
156
|
March 11, 2022
|
|
Verify a intrusive linked list is memory safe with Coq
|
|
4
|
274
|
March 7, 2022
|
|
How to activate the messages window in vscode like the coqide has?
|
|
1
|
220
|
March 5, 2022
|
|
Help with notations that "look alike"
|
|
2
|
141
|
March 4, 2022
|
|
Coqtop not found
|
|
10
|
2340
|
March 3, 2022
|
|
How to create a Powerset of MSetList?
|
|
2
|
186
|
February 24, 2022
|
|
How to use coqc's `verbose` option?
|
|
0
|
123
|
February 23, 2022
|
|
How to install Coq when it says the repository cannot be found? (e.g. issues with m1 chip mac, apple)
|
|
21
|
727
|
February 17, 2022
|
|
Applying a theorem that doesn't match exactly
|
|
4
|
186
|
February 6, 2022
|
|
How to assume an identifier bound to a type with decidable equality using Coq.Structures.Equalities?
|
|
2
|
216
|
January 29, 2022
|
|
Ill-formed recursive definition using `let fix`
|
|
2
|
245
|
January 25, 2022
|
|
Building a project with coq_makefile, using a library specified in .coqrc
|
|
0
|
162
|
January 25, 2022
|
|
Prooving the length of a list under constraint
|
|
8
|
328
|
January 25, 2022
|
|
Coq QuickChick : Making propery Checkable, Decidable, Arbitrary (Gen)
|
|
2
|
204
|
January 20, 2022
|