|
About the Learning category
|
|
1
|
561
|
February 12, 2019
|
|
Failing to prove that substituting "by hand" is equivalent to... well, substituting
|
|
2
|
59
|
November 13, 2021
|
|
Existentially quantified coinductive predicates
|
|
2
|
76
|
November 5, 2021
|
|
Notation for a coinductive type
|
|
1
|
62
|
November 4, 2021
|
|
'rewrite' doesn't want to match large expression
|
|
1
|
43
|
November 2, 2021
|
|
Tvals in my code is the total map, why coq insists it is not?
|
|
3
|
60
|
November 2, 2021
|
|
Constructing heterogeneous lists
|
|
4
|
73
|
October 26, 2021
|
|
Thinking of using hammer/automation to guide the order of proving lemmas
|
|
0
|
55
|
October 24, 2021
|
|
Importing with aliasing
|
|
2
|
61
|
October 16, 2021
|
|
Definitions completed with proof scripts are opaque, how to make them compute
|
|
2
|
63
|
October 15, 2021
|
|
Instances created with ':= ltac:(_)' are much slower than Definitions
|
|
1
|
75
|
October 15, 2021
|
|
Newbie Needs Tutor on ZOOM
|
|
1
|
81
|
October 14, 2021
|
|
Does Universe Polymorphism extend the theory of Coq?
|
|
5
|
114
|
October 1, 2021
|
|
Overload list notation
|
|
3
|
106
|
September 27, 2021
|
|
Dune + proof general
|
|
3
|
141
|
September 23, 2021
|
|
Why the tactic "apply... with..." cannot be applied to hypotheses?
|
|
8
|
111
|
September 23, 2021
|
|
Can the Equations plugin generate a graph that does not reference the original function?
|
|
1
|
97
|
September 22, 2021
|
|
Coqtop not found
|
|
9
|
1100
|
September 21, 2021
|
|
An awkward inductive definition that resists `destruct`
|
|
1
|
87
|
September 20, 2021
|
|
How to define the SEP(R) clauses?
|
|
0
|
65
|
September 20, 2021
|
|
Awkwardness with coinductive universes
|
|
2
|
94
|
September 17, 2021
|
|
How to use tactic forward_if Q?
|
|
4
|
105
|
September 16, 2021
|
|
How to prove this self-defined Bag Theorem?
|
|
5
|
237
|
August 8, 2021
|
|
A question of understanding the paper "Parametric Higher-Order Abstract Syntax for Mechanized Semantics"
|
|
2
|
131
|
August 5, 2021
|
|
Dealing with associativity in reduction relations
|
|
4
|
98
|
August 1, 2021
|
|
Extraction - System error
|
|
8
|
141
|
July 30, 2021
|
|
Software Foundations: minustwo not found in Poly.v
|
|
6
|
133
|
July 28, 2021
|
|
Software Foundations: Normalization Function Exercise
|
|
2
|
103
|
July 26, 2021
|
|
Coq Prove code security
|
|
1
|
135
|
July 26, 2021
|
|
Extraction to Haskell Int type
|
|
2
|
220
|
July 26, 2021
|
