|
Definitions completed with proof scripts are opaque, how to make them compute
|
|
2
|
553
|
October 15, 2021
|
|
Instances created with ':= ltac:(_)' are much slower than Definitions
|
|
1
|
523
|
October 15, 2021
|
|
Newbie Needs Tutor on ZOOM
|
|
1
|
663
|
October 14, 2021
|
|
Does Universe Polymorphism extend the theory of Coq?
|
|
5
|
992
|
October 1, 2021
|
|
Overload list notation
|
|
3
|
1122
|
September 27, 2021
|
|
Dune + proof general
|
|
3
|
892
|
September 23, 2021
|
|
Why the tactic "apply... with..." cannot be applied to hypotheses?
|
|
8
|
1365
|
September 23, 2021
|
|
Can the Equations plugin generate a graph that does not reference the original function?
|
|
1
|
554
|
September 22, 2021
|
|
An awkward inductive definition that resists `destruct`
|
|
1
|
693
|
September 20, 2021
|
|
Awkwardness with coinductive universes
|
|
2
|
496
|
September 17, 2021
|
|
How to use tactic forward_if Q?
|
|
4
|
802
|
September 16, 2021
|
|
How to prove this self-defined Bag Theorem?
|
|
5
|
1394
|
August 8, 2021
|
|
A question of understanding the paper "Parametric Higher-Order Abstract Syntax for Mechanized Semantics"
|
|
2
|
679
|
August 5, 2021
|
|
Dealing with associativity in reduction relations
|
|
4
|
545
|
August 1, 2021
|
|
Extraction - System error
|
|
8
|
928
|
July 30, 2021
|
|
Software Foundations: minustwo not found in Poly.v
|
|
6
|
761
|
July 28, 2021
|
|
Software Foundations: Normalization Function Exercise
|
|
2
|
1593
|
July 26, 2021
|
|
Coq Prove code security
|
|
1
|
742
|
July 26, 2021
|
|
Extraction to Haskell Int type
|
|
2
|
733
|
July 26, 2021
|
|
Evaluating Real numbers to decimal representation
|
|
4
|
778
|
July 26, 2021
|
|
Defining and working with trivial finite sets like {x, y, z} easily
|
|
6
|
780
|
July 8, 2021
|
|
Software foundations: stuck at exercise `binary_inverse` in the Induction chapter
|
|
2
|
940
|
July 6, 2021
|
|
Why is the crush tactic not found?
|
|
1
|
665
|
July 4, 2021
|
|
Does Coq do alpha conversion on it's own?
|
|
2
|
615
|
June 28, 2021
|
|
Need help to define CoFixpoint
|
|
1
|
611
|
June 21, 2021
|
|
What is the syntax to give an explicit proof object (lambda term) to a lemma in Coq?
|
|
5
|
1123
|
June 18, 2021
|
|
Cannot guess decreasing argument of fix
|
|
4
|
2193
|
June 13, 2021
|
|
Cannot coerce aeval to an evaluable reference
|
|
1
|
536
|
June 13, 2021
|
|
Verifiable C: Getting the front element in a linked list based queue
|
|
0
|
718
|
June 5, 2021
|
|
Using exists in pair proof
|
|
4
|
513
|
May 30, 2021
|