|
About the Learning category
|
|
1
|
549
|
February 12, 2019
|
|
Constructing heterogeneous lists
|
|
3
|
32
|
October 25, 2021
|
|
Thinking of using hammer/automation to guide the order of proving lemmas
|
|
0
|
14
|
October 24, 2021
|
|
Notation for a coinductive type
|
|
0
|
18
|
October 22, 2021
|
|
Importing with aliasing
|
|
2
|
48
|
October 16, 2021
|
|
Definitions completed with proof scripts are opaque, how to make them compute
|
|
2
|
40
|
October 15, 2021
|
|
Instances created with ':= ltac:(_)' are much slower than Definitions
|
|
1
|
59
|
October 15, 2021
|
|
Newbie Needs Tutor on ZOOM
|
|
1
|
56
|
October 14, 2021
|
|
Does Universe Polymorphism extend the theory of Coq?
|
|
5
|
93
|
October 1, 2021
|
|
Overload list notation
|
|
3
|
93
|
September 27, 2021
|
|
Dune + proof general
|
|
3
|
121
|
September 23, 2021
|
|
Why the tactic "apply... with..." cannot be applied to hypotheses?
|
|
8
|
95
|
September 23, 2021
|
|
Can the Equations plugin generate a graph that does not reference the original function?
|
|
1
|
87
|
September 22, 2021
|
|
Coqtop not found
|
|
9
|
933
|
September 21, 2021
|
|
An awkward inductive definition that resists `destruct`
|
|
1
|
75
|
September 20, 2021
|
|
How to define the SEP(R) clauses?
|
|
0
|
56
|
September 20, 2021
|
|
Awkwardness with coinductive universes
|
|
2
|
84
|
September 17, 2021
|
|
How to use tactic forward_if Q?
|
|
4
|
76
|
September 16, 2021
|
|
How to prove this self-defined Bag Theorem?
|
|
5
|
183
|
August 8, 2021
|
|
A question of understanding the paper "Parametric Higher-Order Abstract Syntax for Mechanized Semantics"
|
|
2
|
118
|
August 5, 2021
|
|
Dealing with associativity in reduction relations
|
|
4
|
91
|
August 1, 2021
|
|
Extraction - System error
|
|
8
|
127
|
July 30, 2021
|
|
Software Foundations: minustwo not found in Poly.v
|
|
6
|
116
|
July 28, 2021
|
|
Software Foundations: Normalization Function Exercise
|
|
2
|
88
|
July 26, 2021
|
|
Coq Prove code security
|
|
1
|
118
|
July 26, 2021
|
|
Extraction to Haskell Int type
|
|
2
|
213
|
July 26, 2021
|
|
Evaluating Real numbers to decimal representation
|
|
4
|
182
|
July 26, 2021
|
|
Defining and working with trivial finite sets like {x, y, z} easily
|
|
6
|
145
|
July 8, 2021
|
|
Software foundations: stuck at exercise `binary_inverse` in the Induction chapter
|
|
2
|
120
|
July 6, 2021
|
|
Redefining prod as a record?
|
|
1
|
112
|
July 4, 2021
|
