|
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
|
