|
Coq QuickChick : Making propery Checkable, Decidable, Arbitrary (Gen)
|
|
2
|
134
|
January 20, 2022
|
|
QuickChick : forAll and forAllShrink for binary functions
|
|
1
|
140
|
January 18, 2022
|
|
Difference between P -> Q and P /\ Q
|
|
7
|
182
|
January 17, 2022
|
|
SAT solver with a dependent type that guarantees its correctness
|
|
5
|
267
|
January 5, 2022
|
|
Redefining prod as a record?
|
|
3
|
273
|
December 22, 2021
|
|
Confused about nested inductive coinductive types
|
|
3
|
190
|
December 21, 2021
|
|
How to use a local installation of Coq
|
|
6
|
208
|
December 17, 2021
|
|
Html/PDF documentation building with dune
|
|
1
|
131
|
December 16, 2021
|
|
Induction with (deprecated) even
|
|
4
|
134
|
December 7, 2021
|
|
Failing to prove that substituting "by hand" is equivalent to... well, substituting
|
|
2
|
156
|
November 13, 2021
|
|
Existentially quantified coinductive predicates
|
|
2
|
151
|
November 5, 2021
|
|
Notation for a coinductive type
|
|
1
|
150
|
November 4, 2021
|
|
'rewrite' doesn't want to match large expression
|
|
1
|
119
|
November 2, 2021
|
|
Tvals in my code is the total map, why coq insists it is not?
|
|
3
|
138
|
November 2, 2021
|
|
Constructing heterogeneous lists
|
|
4
|
148
|
October 26, 2021
|
|
Thinking of using hammer/automation to guide the order of proving lemmas
|
|
0
|
117
|
October 24, 2021
|
|
Importing with aliasing
|
|
2
|
129
|
October 16, 2021
|
|
Definitions completed with proof scripts are opaque, how to make them compute
|
|
2
|
159
|
October 15, 2021
|
|
Instances created with ':= ltac:(_)' are much slower than Definitions
|
|
1
|
147
|
October 15, 2021
|
|
Newbie Needs Tutor on ZOOM
|
|
1
|
167
|
October 14, 2021
|
|
Does Universe Polymorphism extend the theory of Coq?
|
|
5
|
235
|
October 1, 2021
|
|
Overload list notation
|
|
3
|
193
|
September 27, 2021
|
|
Dune + proof general
|
|
3
|
296
|
September 23, 2021
|
|
Why the tactic "apply... with..." cannot be applied to hypotheses?
|
|
8
|
235
|
September 23, 2021
|
|
Can the Equations plugin generate a graph that does not reference the original function?
|
|
1
|
174
|
September 22, 2021
|
|
An awkward inductive definition that resists `destruct`
|
|
1
|
157
|
September 20, 2021
|
|
How to define the SEP(R) clauses?
|
|
0
|
131
|
September 20, 2021
|
|
Awkwardness with coinductive universes
|
|
2
|
169
|
September 17, 2021
|
|
How to use tactic forward_if Q?
|
|
4
|
197
|
September 16, 2021
|
|
How to prove this self-defined Bag Theorem?
|
|
5
|
439
|
August 8, 2021
|