|
Indeterminate value for partial functions trick
|
|
4
|
734
|
March 14, 2022
|
|
Stream of non-empty lists to stream
|
|
2
|
549
|
March 11, 2022
|
|
Verify a intrusive linked list is memory safe with Coq
|
|
4
|
1086
|
March 7, 2022
|
|
How to activate the messages window in vscode like the coqide has?
|
|
1
|
1020
|
March 5, 2022
|
|
Help with notations that "look alike"
|
|
2
|
547
|
March 4, 2022
|
|
How to create a Powerset of MSetList?
|
|
2
|
810
|
February 24, 2022
|
|
How to use coqc's `verbose` option?
|
|
0
|
437
|
February 23, 2022
|
|
How to install Coq when it says the repository cannot be found? (e.g. issues with m1 chip mac, apple)
|
|
21
|
3985
|
February 17, 2022
|
|
Applying a theorem that doesn't match exactly
|
|
4
|
578
|
February 6, 2022
|
|
How to assume an identifier bound to a type with decidable equality using Coq.Structures.Equalities?
|
|
2
|
661
|
January 29, 2022
|
|
Ill-formed recursive definition using `let fix`
|
|
2
|
1169
|
January 25, 2022
|
|
Building a project with coq_makefile, using a library specified in .coqrc
|
|
0
|
735
|
January 25, 2022
|
|
Prooving the length of a list under constraint
|
|
8
|
1312
|
January 25, 2022
|
|
Coq QuickChick : Making propery Checkable, Decidable, Arbitrary (Gen)
|
|
2
|
647
|
January 20, 2022
|
|
QuickChick : forAll and forAllShrink for binary functions
|
|
1
|
557
|
January 18, 2022
|
|
Difference between P -> Q and P /\ Q
|
|
7
|
1620
|
January 17, 2022
|
|
SAT solver with a dependent type that guarantees its correctness
|
|
5
|
1043
|
January 5, 2022
|
|
Redefining prod as a record?
|
|
3
|
835
|
December 22, 2021
|
|
Confused about nested inductive coinductive types
|
|
3
|
643
|
December 21, 2021
|
|
How to use a local installation of Coq
|
|
6
|
788
|
December 17, 2021
|
|
Html/PDF documentation building with dune
|
|
1
|
736
|
December 16, 2021
|
|
Induction with (deprecated) even
|
|
4
|
831
|
December 7, 2021
|
|
Failing to prove that substituting "by hand" is equivalent to... well, substituting
|
|
2
|
514
|
November 13, 2021
|
|
Existentially quantified coinductive predicates
|
|
2
|
559
|
November 5, 2021
|
|
Notation for a coinductive type
|
|
1
|
507
|
November 4, 2021
|
|
'rewrite' doesn't want to match large expression
|
|
1
|
566
|
November 2, 2021
|
|
Tvals in my code is the total map, why coq insists it is not?
|
|
3
|
724
|
November 2, 2021
|
|
Constructing heterogeneous lists
|
|
4
|
801
|
October 26, 2021
|
|
Thinking of using hammer/automation to guide the order of proving lemmas
|
|
0
|
451
|
October 24, 2021
|
|
Importing with aliasing
|
|
2
|
566
|
October 16, 2021
|