|
About the Learning category
|
|
1
|
504
|
February 12, 2019
|
|
Software Foundations: minustwo not found in Poly.v
|
|
5
|
39
|
July 27, 2021
|
|
Software Foundations: Normalization Function Exercise
|
|
2
|
17
|
July 26, 2021
|
|
Coq Prove code security
|
|
1
|
33
|
July 26, 2021
|
|
Extraction to Haskell Int type
|
|
2
|
166
|
July 26, 2021
|
|
Evaluating Real numbers to decimal representation
|
|
4
|
131
|
July 26, 2021
|
|
Defining and working with trivial finite sets like {x, y, z} easily
|
|
6
|
83
|
July 8, 2021
|
|
Software foundations: stuck at exercise `binary_inverse` in the Induction chapter
|
|
2
|
48
|
July 6, 2021
|
|
Redefining prod as a record?
|
|
1
|
70
|
July 4, 2021
|
|
Why is the crush tactic not found?
|
|
1
|
46
|
July 4, 2021
|
|
Does Coq do alpha conversion on it's own?
|
|
2
|
69
|
June 28, 2021
|
|
How to unset printing everything? (e.g. implicits, notations, etc)
|
|
5
|
64
|
June 25, 2021
|
|
Coqtop not found
|
|
8
|
625
|
June 23, 2021
|
|
Need help to define CoFixpoint
|
|
1
|
81
|
June 21, 2021
|
|
What is the syntax to give an explicit proof object (lambda term) to a lemma in Coq?
|
|
5
|
60
|
June 18, 2021
|
|
Cannot guess decreasing argument of fix
|
|
4
|
61
|
June 13, 2021
|
|
Cannot coerce aeval to an evaluable reference
|
|
1
|
45
|
June 13, 2021
|
|
Verifiable C: Getting the front element in a linked list based queue
|
|
0
|
68
|
June 5, 2021
|
|
Using exists in pair proof
|
|
4
|
90
|
May 30, 2021
|
|
Strong specification of haskell's Replicate function
|
|
1
|
80
|
May 23, 2021
|
|
Diamond property implies confluence
|
|
11
|
635
|
May 21, 2021
|
|
Why Coq cannot compute the equality of two Real number (like R1,1,2,3) directly?
|
|
2
|
127
|
May 17, 2021
|
|
Finding the right tactics to proof a theorem
|
|
1
|
94
|
May 10, 2021
|
|
Should we need Coq on Android?
|
|
2
|
150
|
May 4, 2021
|
|
Passing parameters to coqc in dune
|
|
4
|
185
|
April 19, 2021
|
|
Applying a tactic in depth-first manner
|
|
0
|
145
|
April 19, 2021
|
|
Tactics for pattern matching?
|
|
3
|
211
|
April 17, 2021
|
|
Apparently bad installation of coq (im a newbie)
|
|
5
|
222
|
April 16, 2021
|
|
Proving matrix transpose function
|
|
13
|
575
|
April 14, 2021
|
|
Turning "exists unique" into a function in Coq
|
|
3
|
261
|
April 3, 2021
|
