|
Annoying warnings when Requiring/Importing ssreflect
|
|
4
|
218
|
March 28, 2022
|
|
Inductive proof automation
|
|
6
|
680
|
March 25, 2022
|
|
What is a hammer/atp within the logic of coq that does things like induction in coq?
|
|
1
|
196
|
March 24, 2022
|
|
How to state mutual/nested lemmas
|
|
8
|
497
|
March 22, 2022
|
|
Saerch in VSCoq
|
|
5
|
275
|
March 22, 2022
|
|
Stdlib documentation online?
|
|
1
|
161
|
March 20, 2022
|
|
More informative response to stucked proofs?
|
|
3
|
244
|
March 18, 2022
|
|
Indeterminate value for partial functions trick
|
|
4
|
342
|
March 14, 2022
|
|
Stream of non-empty lists to stream
|
|
2
|
241
|
March 11, 2022
|
|
Verify a intrusive linked list is memory safe with Coq
|
|
4
|
458
|
March 7, 2022
|
|
How to activate the messages window in vscode like the coqide has?
|
|
1
|
418
|
March 5, 2022
|
|
Help with notations that "look alike"
|
|
2
|
221
|
March 4, 2022
|
|
Coqtop not found
|
|
10
|
3222
|
March 3, 2022
|
|
How to create a Powerset of MSetList?
|
|
2
|
284
|
February 24, 2022
|
|
How to use coqc's `verbose` option?
|
|
0
|
192
|
February 23, 2022
|
|
How to install Coq when it says the repository cannot be found? (e.g. issues with m1 chip mac, apple)
|
|
21
|
1348
|
February 17, 2022
|
|
Applying a theorem that doesn't match exactly
|
|
4
|
265
|
February 6, 2022
|
|
How to assume an identifier bound to a type with decidable equality using Coq.Structures.Equalities?
|
|
2
|
308
|
January 29, 2022
|
|
Ill-formed recursive definition using `let fix`
|
|
2
|
493
|
January 25, 2022
|
|
Building a project with coq_makefile, using a library specified in .coqrc
|
|
0
|
242
|
January 25, 2022
|
|
Prooving the length of a list under constraint
|
|
8
|
510
|
January 25, 2022
|
|
Coq QuickChick : Making propery Checkable, Decidable, Arbitrary (Gen)
|
|
2
|
286
|
January 20, 2022
|
|
QuickChick : forAll and forAllShrink for binary functions
|
|
1
|
281
|
January 18, 2022
|
|
Difference between P -> Q and P /\ Q
|
|
7
|
394
|
January 17, 2022
|
|
SAT solver with a dependent type that guarantees its correctness
|
|
5
|
529
|
January 5, 2022
|
|
Redefining prod as a record?
|
|
3
|
476
|
December 22, 2021
|
|
Confused about nested inductive coinductive types
|
|
3
|
331
|
December 21, 2021
|
|
How to use a local installation of Coq
|
|
6
|
383
|
December 17, 2021
|
|
Html/PDF documentation building with dune
|
|
1
|
361
|
December 16, 2021
|
|
Induction with (deprecated) even
|
|
4
|
333
|
December 7, 2021
|