|
About the Learning category
|
|
1
|
527
|
February 12, 2019
|
|
Simple recursive proof
|
|
0
|
16
|
September 17, 2021
|
|
Dune + proof general
|
|
2
|
50
|
September 18, 2021
|
|
Awkwardness with coinductive universes
|
|
2
|
42
|
September 17, 2021
|
|
How to use tactic forward_if Q?
|
|
4
|
40
|
September 16, 2021
|
|
How to prove this self-defined Bag Theorem?
|
|
5
|
127
|
August 8, 2021
|
|
A question of understanding the paper "Parametric Higher-Order Abstract Syntax for Mechanized Semantics"
|
|
2
|
98
|
August 5, 2021
|
|
Dealing with associativity in reduction relations
|
|
4
|
75
|
August 1, 2021
|
|
Extraction - System error
|
|
8
|
109
|
July 30, 2021
|
|
Software Foundations: minustwo not found in Poly.v
|
|
6
|
91
|
July 28, 2021
|
|
Software Foundations: Normalization Function Exercise
|
|
2
|
70
|
July 26, 2021
|
|
Coq Prove code security
|
|
1
|
99
|
July 26, 2021
|
|
Extraction to Haskell Int type
|
|
2
|
194
|
July 26, 2021
|
|
Evaluating Real numbers to decimal representation
|
|
4
|
168
|
July 26, 2021
|
|
Defining and working with trivial finite sets like {x, y, z} easily
|
|
6
|
130
|
July 8, 2021
|
|
Software foundations: stuck at exercise `binary_inverse` in the Induction chapter
|
|
2
|
86
|
July 6, 2021
|
|
Redefining prod as a record?
|
|
1
|
95
|
July 4, 2021
|
|
Why is the crush tactic not found?
|
|
1
|
73
|
July 4, 2021
|
|
Does Coq do alpha conversion on it's own?
|
|
2
|
97
|
June 28, 2021
|
|
How to unset printing everything? (e.g. implicits, notations, etc)
|
|
5
|
100
|
June 25, 2021
|
|
Coqtop not found
|
|
8
|
777
|
June 23, 2021
|
|
Need help to define CoFixpoint
|
|
1
|
101
|
June 21, 2021
|
|
What is the syntax to give an explicit proof object (lambda term) to a lemma in Coq?
|
|
5
|
94
|
June 18, 2021
|
|
Cannot guess decreasing argument of fix
|
|
4
|
121
|
June 13, 2021
|
|
Cannot coerce aeval to an evaluable reference
|
|
1
|
58
|
June 13, 2021
|
|
Verifiable C: Getting the front element in a linked list based queue
|
|
0
|
91
|
June 5, 2021
|
|
Using exists in pair proof
|
|
4
|
103
|
May 30, 2021
|
|
Strong specification of haskell's Replicate function
|
|
1
|
94
|
May 23, 2021
|
|
Diamond property implies confluence
|
|
11
|
685
|
May 21, 2021
|
|
Why Coq cannot compute the equality of two Real number (like R1,1,2,3) directly?
|
|
2
|
150
|
May 17, 2021
|
