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 selfdefined Bag Theorem?


5

439

August 8, 2021
