Polymorphic seq


1

81

May 24, 2024

Strange failure of general rewriting


0

74

May 24, 2024

Strange failure in typeclass resolution


2

92

May 22, 2024

Installation attempts on MacbookPro M3 Max give Segmentation fault: 11 errors


1

81

May 22, 2024

Which library to formalise undergrad math?


2

104

May 17, 2024

Coq crashes too frequently


3

152

May 14, 2024

Using Coq to prove Lagrange's Theorem


1

121

May 12, 2024

Typeclass search with lambda in parameter


2

80

May 10, 2024

Is there a reference for using tactics in Coq so that the size of a proof is significantly reduced?


1

77

May 9, 2024

Problem with notation in CPS ceval_step extension of LF's ImpCEvalFun


2

97

May 9, 2024

Exact_no_check fails on Type


3

82

May 8, 2024

Proof if then else function with if hypothesis


4

142

May 7, 2024

Can we prove the following theorem constructively, and if not, what axioms are needed?


4

133

April 29, 2024

Is there a way to create binary floats from hexadecimals?


1

112

April 22, 2024

Replacing "true = false"


3

189

April 11, 2024

Ologs in Coq


0

115

April 10, 2024

How to simplify singlebranch match expressions?


2

210

April 8, 2024

Https://coq.inria.fr/opam/released is down


3

114

April 8, 2024

How to use binary floats in Flocq


3

169

April 5, 2024

How to proof a simple statement about rational numbers


4

271

March 26, 2024

How to automatically extract anonymous subterms in a goal


0

136

March 19, 2024

Ltac with variadic argument


1

209

March 4, 2024

[Question; very basic] Stackbased virtual machine test


2

240

March 1, 2024

Destructing term when match generates equality involving that term


5

252

February 20, 2024

Negative definitions of coinductive propositions


2

214

February 19, 2024

Is constructive indefinite description a conservative extension?


4

200

February 13, 2024

Induction hypotheses, again


4

179

February 9, 2024

Coq examples of cut elimination in sequent calculi?


2

244

February 8, 2024

Simplifying/rewriting inside of an anonymous fixpoint


0

197

February 6, 2024

Dependenttyped terms as return values / function parameters


3

267

February 2, 2024
