|
Good library or framework for handling extraction, IO, etc?
|
|
3
|
668
|
July 10, 2020
|
|
Asser assume differ
|
|
1
|
1304
|
July 9, 2020
|
|
How to Use a Definition in a Proof?
|
|
6
|
1625
|
July 8, 2020
|
|
Suggested Answers
|
|
1
|
1232
|
July 7, 2020
|
|
Where does CompCert fall short?
|
|
2
|
849
|
July 6, 2020
|
|
Arguments in tactics
|
|
1
|
590
|
July 5, 2020
|
|
Confused with a failure of a generalized rewrite
|
|
8
|
2308
|
July 1, 2020
|
|
Setoid rewriting with implications
|
|
1
|
803
|
July 1, 2020
|
|
Simplify proofs with neested pattern matching
|
|
1
|
761
|
June 30, 2020
|
|
What's a convenient way to install multiple Coq versions side by side?
|
|
7
|
2070
|
June 29, 2020
|
|
Programmable hint databases with Ltac2
|
|
0
|
699
|
June 22, 2020
|
|
Typeclasses: considered harmful? Idiomatic?
|
|
2
|
1522
|
June 21, 2020
|
|
Using the Proof assistant for probability and learning theory? How to get started?
|
|
1
|
1101
|
June 19, 2020
|
|
Naive quotients of types?
|
|
4
|
1143
|
June 17, 2020
|
|
No such contradiction error
|
|
2
|
757
|
June 16, 2020
|
|
Prove some simple laws
|
|
3
|
818
|
June 12, 2020
|
|
Software Foundation Hoare solution
|
|
1
|
1021
|
June 11, 2020
|
|
How to import a file in Coq?
|
|
6
|
4621
|
June 8, 2020
|
|
MetaOCaml in Coq
|
|
0
|
480
|
June 7, 2020
|
|
"Coordinates" in tree-like structure
|
|
1
|
563
|
June 6, 2020
|
|
How to prove that every real number is bounded above by some natural number?
|
|
1
|
548
|
May 27, 2020
|
|
Use notation defined in module type
|
|
2
|
1097
|
May 27, 2020
|
|
Proving transpose function: now refactored!
|
|
9
|
1416
|
May 26, 2020
|
|
Arbitrary types in Dependent Pattern Matching
|
|
9
|
1585
|
May 25, 2020
|
|
Need guidance on proving a lemma
|
|
2
|
1252
|
May 20, 2020
|
|
Dependent definition of interval?
|
|
3
|
761
|
May 19, 2020
|
|
Mutual Induction Processing Slowdown
|
|
13
|
1236
|
May 19, 2020
|
|
Decidable equality on multiply nested inductives
|
|
4
|
1077
|
May 13, 2020
|
|
Idea to add "index" function to Standard Library (or maybe not)
|
|
4
|
1062
|
May 8, 2020
|
|
How to get the power of 2 working
|
|
6
|
993
|
May 8, 2020
|