|
What's a convenient way to install multiple Coq versions side by side?
|
|
8
|
129
|
June 29, 2020
|
|
Programmable hint databases with Ltac2
|
|
1
|
92
|
June 22, 2020
|
|
Typeclasses: considered harmful? Idiomatic?
|
|
3
|
164
|
June 21, 2020
|
|
Using the Proof assistant for probability and learning theory? How to get started?
|
|
2
|
91
|
June 19, 2020
|
|
Naive quotients of types?
|
|
5
|
124
|
June 17, 2020
|
|
No such contradiction error
|
|
3
|
88
|
June 16, 2020
|
|
Prove some simple laws
|
|
4
|
111
|
June 12, 2020
|
|
Software Foundation Hoare solution
|
|
2
|
90
|
June 11, 2020
|
|
How to import a file in Coq?
|
|
7
|
131
|
June 8, 2020
|
|
MetaOCaml in Coq
|
|
1
|
73
|
June 7, 2020
|
|
"Coordinates" in tree-like structure
|
|
2
|
72
|
June 6, 2020
|
|
Mutual Recursion with function unfolding
|
|
3
|
87
|
June 4, 2020
|
|
How to prove that every real number is bounded above by some natural number?
|
|
2
|
98
|
May 27, 2020
|
|
Use notation defined in module type
|
|
3
|
138
|
May 27, 2020
|
|
Proving transpose function: now refactored!
|
|
10
|
171
|
May 26, 2020
|
|
Coqtop not found
|
|
7
|
104
|
May 26, 2020
|
|
Arbitrary types in Dependent Pattern Matching
|
|
10
|
157
|
May 25, 2020
|
|
Need guidance on proving a lemma
|
|
3
|
103
|
May 20, 2020
|
|
Dependent definition of interval?
|
|
4
|
98
|
May 19, 2020
|
|
Mutual Induction Processing Slowdown
|
|
14
|
208
|
May 19, 2020
|
|
Decidable equality on multiply nested inductives
|
|
5
|
176
|
May 13, 2020
|
|
Idea to add "index" function to Standard Library (or maybe not)
|
|
5
|
104
|
May 8, 2020
|
|
How to get the power of 2 working
|
|
7
|
123
|
May 8, 2020
|
|
How to apply hypothesis with a disjunction?
|
|
4
|
86
|
May 8, 2020
|
|
Proving matrix transpose function
|
|
13
|
196
|
May 7, 2020
|
|
Why does the entire body of a cofix need to be guarded?
|
|
4
|
96
|
May 6, 2020
|
|
Deprecated
|
|
7
|
143
|
May 6, 2020
|
|
Yet another simple theorem
|
|
9
|
140
|
May 4, 2020
|
|
Compute a bijection (A <~> B) from a bijection (option A <~> option B)
|
|
7
|
156
|
May 3, 2020
|
|
Asymmetric variant of program equivalence : Program approximation
|
|
5
|
123
|
May 2, 2020
|
