|
Applying hypothesis with unknown variables
|
|
1
|
80
|
July 31, 2020
|
|
Software Foundations/Logical Foundations Exercise
|
|
2
|
141
|
July 30, 2020
|
|
Hint databases as argument
|
|
5
|
164
|
July 27, 2020
|
|
Cbn vs simpl?
|
|
2
|
246
|
July 23, 2020
|
|
Why Coq does not allow the containment relationship between types
|
|
3
|
184
|
July 23, 2020
|
|
Create a definition using a proof script inside a proof script
|
|
3
|
120
|
July 21, 2020
|
|
(Finite, discrete) Probabilities in Coq?
|
|
9
|
1094
|
July 17, 2020
|
|
Nested dependent pattern matching
|
|
1
|
122
|
July 14, 2020
|
|
Parsing Tactics via SerAPI
|
|
4
|
139
|
July 13, 2020
|
|
Hyperlink in coqdoc
|
|
1
|
194
|
July 12, 2020
|
|
Formally verified pieces of the network stack? (eg RPC)
|
|
3
|
145
|
July 12, 2020
|
|
Tacarg in Ltac
|
|
1
|
100
|
July 10, 2020
|
|
Good library or framework for handling extraction, IO, etc?
|
|
3
|
119
|
July 10, 2020
|
|
Asser assume differ
|
|
1
|
146
|
July 9, 2020
|
|
How to Use a Definition in a Proof?
|
|
6
|
211
|
July 8, 2020
|
|
Suggested Answers
|
|
1
|
107
|
July 7, 2020
|
|
Where does CompCert fall short?
|
|
2
|
193
|
July 6, 2020
|
|
Arguments in tactics
|
|
1
|
87
|
July 5, 2020
|
|
Confused with a failure of a generalized rewrite
|
|
8
|
464
|
July 1, 2020
|
|
Setoid rewriting with implications
|
|
1
|
132
|
July 1, 2020
|
|
Simplify proofs with neested pattern matching
|
|
1
|
131
|
June 30, 2020
|
|
What's a convenient way to install multiple Coq versions side by side?
|
|
7
|
324
|
June 29, 2020
|
|
Programmable hint databases with Ltac2
|
|
0
|
162
|
June 22, 2020
|
|
Typeclasses: considered harmful? Idiomatic?
|
|
2
|
279
|
June 21, 2020
|
|
Using the Proof assistant for probability and learning theory? How to get started?
|
|
1
|
169
|
June 19, 2020
|
|
Naive quotients of types?
|
|
4
|
214
|
June 17, 2020
|
|
No such contradiction error
|
|
2
|
130
|
June 16, 2020
|
|
Prove some simple laws
|
|
3
|
210
|
June 12, 2020
|
|
Software Foundation Hoare solution
|
|
1
|
156
|
June 11, 2020
|
|
How to import a file in Coq?
|
|
6
|
443
|
June 8, 2020
|
