|
About the Learning category
|
|
1
|
483
|
February 12, 2019
|
|
What is the syntax to give an explicit proof object (lambda term) to a lemma in Coq?
|
|
5
|
17
|
June 18, 2021
|
|
Coqtop not found
|
|
7
|
542
|
June 17, 2021
|
|
Cannot guess decreasing argument of fix
|
|
4
|
39
|
June 13, 2021
|
|
Cannot coerce aeval to an evaluable reference
|
|
1
|
30
|
June 13, 2021
|
|
Verifiable C: Getting the front element in a linked list based queue
|
|
0
|
52
|
June 5, 2021
|
|
Using exists in pair proof
|
|
4
|
79
|
May 30, 2021
|
|
Evaluating Real numbers to decimal representation
|
|
3
|
86
|
May 26, 2021
|
|
Strong specification of haskell's Replicate function
|
|
1
|
65
|
May 23, 2021
|
|
Diamond property implies confluence
|
|
11
|
592
|
May 21, 2021
|
|
Why Coq cannot compute the equality of two Real number (like R1,1,2,3) directly?
|
|
2
|
108
|
May 17, 2021
|
|
Finding the right tactics to proof a theorem
|
|
1
|
77
|
May 10, 2021
|
|
Should we need Coq on Android?
|
|
2
|
105
|
May 4, 2021
|
|
Passing parameters to coqc in dune
|
|
4
|
165
|
April 19, 2021
|
|
Applying a tactic in depth-first manner
|
|
0
|
138
|
April 19, 2021
|
|
Tactics for pattern matching?
|
|
3
|
198
|
April 17, 2021
|
|
Apparently bad installation of coq (im a newbie)
|
|
5
|
193
|
April 16, 2021
|
|
Proving matrix transpose function
|
|
13
|
540
|
April 14, 2021
|
|
Turning "exists unique" into a function in Coq
|
|
3
|
237
|
April 3, 2021
|
|
Bug in the parser?
|
|
5
|
174
|
April 1, 2021
|
|
Not an inductive product
|
|
5
|
179
|
March 31, 2021
|
|
What axioms are built-in?
|
|
6
|
219
|
March 31, 2021
|
|
What does `auto` do differently under the hood?
|
|
1
|
160
|
March 31, 2021
|
|
Rtauto slower than tauto
|
|
0
|
136
|
March 29, 2021
|
|
How to express a list of any type X?
|
|
2
|
160
|
March 28, 2021
|
|
Solve an `exists` goal in a field with proof search?
|
|
3
|
166
|
March 26, 2021
|
|
Reasoning about higher-order program transformation?
|
|
3
|
184
|
March 26, 2021
|
|
Add LoadPath in Coq 8.12.2
|
|
5
|
251
|
March 22, 2021
|
|
Poll about proofgeneral: do you use "holes"
|
|
0
|
170
|
March 22, 2021
|
|
Defining mathematical function implicitly
|
|
4
|
173
|
March 19, 2021
|
