Is it possible to define binary trees without a new inductive type?


1

141

August 12, 2020

JMeq and dependent programming


4

176

August 9, 2020

Coq Training App


1

128

August 9, 2020

Can't compile packages with coqide


1

57

August 8, 2020

Proving existence statements about coinductive types constructively


1

75

August 4, 2020

Applying hypothesis with unknown variables


1

62

July 31, 2020

Software Foundations/Logical Foundations Exercise


2

99

July 30, 2020

Hint databases as argument


5

119

July 27, 2020

Cbn vs simpl?


2

158

July 23, 2020

Why Coq does not allow the containment relationship between types


3

137

July 23, 2020

Create a definition using a proof script inside a proof script


3

94

July 21, 2020

(Finite, discrete) Probabilities in Coq?


9

907

July 17, 2020

Nested dependent pattern matching


1

89

July 14, 2020

Parsing Tactics via SerAPI


4

117

July 13, 2020

Hyperlink in coqdoc


1

161

July 12, 2020

Formally verified pieces of the network stack? (eg RPC)


3

112

July 12, 2020

Tacarg in Ltac


1

78

July 10, 2020

Good library or framework for handling extraction, IO, etc?


3

93

July 10, 2020

Asser assume differ


1

114

July 9, 2020

How to Use a Definition in a Proof?


6

114

July 8, 2020

Suggested Answers


1

78

July 7, 2020

Where does CompCert fall short?


2

155

July 6, 2020

Arguments in tactics


1

64

July 5, 2020

Confused with a failure of a generalized rewrite


8

319

July 1, 2020

Setoid rewriting with implications


1

90

July 1, 2020

Simplify proofs with neested pattern matching


1

95

June 30, 2020

What's a convenient way to install multiple Coq versions side by side?


7

211

June 29, 2020

Programmable hint databases with Ltac2


0

126

June 22, 2020

Typeclasses: considered harmful? Idiomatic?


2

217

June 21, 2020

Using the Proof assistant for probability and learning theory? How to get started?


1

126

June 19, 2020
