|
About the Learning category
|
|
2
|
293
|
February 12, 2019
|
|
Extended simply typed lyambda calculus substitution for let term
|
|
2
|
23
|
August 14, 2020
|
|
Subtyping in Simply Typed Lambda-Calculus
|
|
6
|
41
|
August 14, 2020
|
|
Spacemacs won't let me retract the proof buffer
|
|
7
|
47
|
August 13, 2020
|
|
Is it possible to define binary trees without a new inductive type?
|
|
2
|
34
|
August 12, 2020
|
|
JMeq and dependent programming
|
|
5
|
123
|
August 9, 2020
|
|
Coq Training App
|
|
2
|
56
|
August 9, 2020
|
|
Can't compile packages with coqide
|
|
2
|
30
|
August 8, 2020
|
|
[install] Notes on Coq and OCaml versions / configuration
|
|
19
|
525
|
August 6, 2020
|
|
Proving existence statements about coinductive types constructively
|
|
2
|
47
|
August 4, 2020
|
|
Notation for inequality chain
|
|
4
|
149
|
August 1, 2020
|
|
Applying hypothesis with unknown variables
|
|
2
|
39
|
July 31, 2020
|
|
Software Foundations/Logical Foundations Exercise
|
|
3
|
64
|
July 30, 2020
|
|
Hint databases as argument
|
|
6
|
77
|
July 27, 2020
|
|
Cbn vs simpl?
|
|
3
|
109
|
July 23, 2020
|
|
Why Coq does not allow the containment relationship between types
|
|
4
|
92
|
July 23, 2020
|
|
Create a definition using a proof script inside a proof script
|
|
4
|
68
|
July 21, 2020
|
|
(Finite, discrete) Probabilities in Coq?
|
|
10
|
789
|
July 17, 2020
|
|
Nested dependent pattern matching
|
|
2
|
56
|
July 14, 2020
|
|
Preventing pollution of the instance context during Import
|
|
9
|
123
|
July 14, 2020
|
|
Parsing Tactics via SerAPI
|
|
5
|
84
|
July 13, 2020
|
|
Hyperlink in coqdoc
|
|
2
|
134
|
July 12, 2020
|
|
Formally verified pieces of the network stack? (eg RPC)
|
|
4
|
85
|
July 12, 2020
|
|
Tacarg in Ltac
|
|
2
|
55
|
July 10, 2020
|
|
Good library or framework for handling extraction, IO, etc?
|
|
4
|
71
|
July 10, 2020
|
|
Asser assume differ
|
|
2
|
84
|
July 9, 2020
|
|
How to Use a Definition in a Proof?
|
|
7
|
75
|
July 8, 2020
|
|
Suggested Answers
|
|
2
|
51
|
July 7, 2020
|
|
Where does CompCert fall short?
|
|
3
|
130
|
July 6, 2020
|
|
Arguments in tactics
|
|
2
|
49
|
July 5, 2020
|
