About the Learning category


1

1106

February 12, 2019

Polymorphic seq


1

27

May 24, 2024

Strange failure of general rewriting


0

20

May 24, 2024

Strange failure in typeclass resolution


2

41

May 22, 2024

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


1

21

May 22, 2024

Writing a Latex document embedding Coq code


4

73

May 18, 2024

Which library to formalise undergrad math?


2

60

May 17, 2024

Coq crashes too frequently


3

61

May 14, 2024

Using Coq to prove Lagrange's Theorem


1

79

May 12, 2024

Typeclass search with lambda in parameter


2

48

May 10, 2024

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


1

49

May 9, 2024

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


2

60

May 9, 2024

Exact_no_check fails on Type


3

44

May 8, 2024

Proof if then else function with if hypothesis


4

57

May 7, 2024

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


4

97

April 29, 2024

Is there a way to create binary floats from hexadecimals?


1

85

April 22, 2024

Replacing "true = false"


3

143

April 11, 2024

Ologs in Coq


0

91

April 10, 2024

How to simplify singlebranch match expressions?


2

111

April 8, 2024

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


3

88

April 8, 2024

How to use binary floats in Flocq


3

115

April 5, 2024

How to proof a simple statement about rational numbers


4

193

March 26, 2024

How to automatically extract anonymous subterms in a goal


0

102

March 19, 2024

Ltac with variadic argument


1

175

March 4, 2024

[Question; very basic] Stackbased virtual machine test


2

197

March 1, 2024

Destructing term when match generates equality involving that term


5

187

February 20, 2024

Negative definitions of coinductive propositions


2

168

February 19, 2024

Is constructive indefinite description a conservative extension?


4

171

February 13, 2024

Induction hypotheses, again


4

152

February 9, 2024

Coq examples of cut elimination in sequent calculi?


2

171

February 8, 2024
