|
About the Learning category
|
|
1
|
775
|
February 12, 2019
|
|
Stuck on destructing
|
|
2
|
37
|
January 17, 2023
|
|
How do I write a summation on Coq?
|
|
2
|
53
|
January 9, 2023
|
|
Problems rewriting with type valued relations
|
|
4
|
64
|
January 7, 2023
|
|
Official place to learn how to setup Coq make files for beginner
|
|
13
|
338
|
December 26, 2022
|
|
Print the curried version of a function (i.e. explicitly printing the functions as an explicit chain)
|
|
3
|
143
|
December 20, 2022
|
|
How to install the coq 8.14 package with opam pin when it says it can't find it?
|
|
1
|
63
|
December 11, 2022
|
|
Understand the reduction behind apply
|
|
3
|
59
|
December 7, 2022
|
|
How does one print proof terms as de bruijn indices instead of random named variables in Coq?
|
|
1
|
107
|
December 6, 2022
|
|
Type (let (a, b) = ... in something a) vs. (something (let (a, b) = ... in a))
|
|
5
|
112
|
November 8, 2022
|
|
Is it possible to share binary-only libraries across OSes?
|
|
5
|
119
|
October 19, 2022
|
|
How to be good in formal verification?
|
|
3
|
194
|
October 7, 2022
|
|
Typeclasses on functions
|
|
1
|
127
|
September 29, 2022
|
|
Can I achieve some specific project with Coq?
|
|
3
|
159
|
September 28, 2022
|
|
Generating latex from coq theorems (Coq to Latex)
|
|
1
|
158
|
September 26, 2022
|
|
What is unsafe about the Ltac2.Constr.Unsafe module?
|
|
2
|
137
|
September 23, 2022
|
|
Modules vs. generalized rewrite
|
|
4
|
116
|
September 19, 2022
|
|
Best way to express that a type is inhabited in a way that allows getting the habitant
|
|
1
|
137
|
September 13, 2022
|
|
Divmod equation
|
|
3
|
98
|
September 11, 2022
|
|
Defining functions in proof mode
|
|
6
|
156
|
September 9, 2022
|
|
"Qed." takes a long time
|
|
7
|
248
|
September 1, 2022
|
|
Coq and denotational semantics
|
|
1
|
124
|
August 27, 2022
|
|
Efficient algorithms using tree
|
|
6
|
140
|
August 21, 2022
|
|
Choosing between SProp and axiomatic proof irrelevance
|
|
11
|
239
|
August 16, 2022
|
|
Is there a solution for the problematic induction hypotheses generated using eqn:H?
|
|
10
|
133
|
August 15, 2022
|
|
Print Module [Type] lacks types
|
|
0
|
87
|
August 14, 2022
|
|
Speed of Program Instance
|
|
0
|
93
|
August 12, 2022
|
|
"Correct" way to structure modules
|
|
2
|
144
|
August 9, 2022
|
|
The reference omega was not found in the current environment
|
|
2
|
243
|
August 1, 2022
|
|
Is it possible to suppose the falsity of the goal and prove False in Coq?
|
|
5
|
234
|
July 28, 2022
|