How to organize a Coq library?


0

155

April 1, 2023

Possible lra bug


3

158

March 28, 2023

Unexpectedly accepted eapply hypothesis


5

153

March 19, 2023

Compute 121393+121393 causes stack overflow


8

211

March 19, 2023

Coqtop Cannot Add File to Load Path


1

108

March 14, 2023

Can I achieve some specific project with Coq?


4

356

March 11, 2023

Is it possible to define a cbnable universe cast with universe checking disabled?


9

138

March 8, 2023

Request for feedback: new convenience tactics/options for deterministic timouts & memory limits in Coq


0

192

March 8, 2023

Survey of category theory in Coq


4

3100

March 4, 2023

How to have vscode find coq?


5

2448

February 24, 2023

How to import Basics.v in Induction.v of LF using VS Coq extension


7

1830

February 24, 2023

Abstract and concrete access to a data structure


0

141

February 22, 2023

Permutation with firstn and skipn


1

141

February 11, 2023

Is there a way to redirect Coqide messages and errors to the same output?


1

143

February 2, 2023

Stuck on destructing


2

173

January 17, 2023

How do I write a summation on Coq?


2

233

January 9, 2023

Problems rewriting with type valued relations


4

185

January 7, 2023

Print the curried version of a function (i.e. explicitly printing the functions as an explicit chain)


3

253

December 20, 2022

How to install the coq 8.14 package with opam pin when it says it can't find it?


1

236

December 11, 2022

Understand the reduction behind apply


3

182

December 7, 2022

How does one print proof terms as de bruijn indices instead of random named variables in Coq?


1

274

December 6, 2022

Type (let (a, b) = ... in something a) vs. (something (let (a, b) = ... in a))


5

232

November 8, 2022

Is it possible to share binaryonly libraries across OSes?


5

309

October 19, 2022

How to be good in formal verification?


3

486

October 7, 2022

Typeclasses on functions


1

251

September 29, 2022

Generating latex from coq theorems (Coq to Latex)


1

410

September 26, 2022

What is unsafe about the Ltac2.Constr.Unsafe module?


2

253

September 23, 2022

Modules vs. generalized rewrite


4

284

September 19, 2022

Best way to express that a type is inhabited in a way that allows getting the habitant


1

255

September 13, 2022

Divmod equation


3

242

September 11, 2022
