|
LL(n) notations in Coq
|
|
15
|
1471
|
October 3, 2020
|
|
Another Proof From Logical Foundations Exercises
|
|
7
|
1844
|
October 1, 2020
|
|
Article latex document class out of a Coq script
|
|
2
|
770
|
September 30, 2020
|
|
Corecursion via destructors?
|
|
2
|
749
|
September 27, 2020
|
|
Software Foundations/ Verified Functional Algorithms Exercise
|
|
1
|
756
|
September 18, 2020
|
|
Coqchk
|
|
9
|
854
|
September 10, 2020
|
|
Preventing pollution of the instance context during Import
|
|
10
|
842
|
September 8, 2020
|
|
A template for organizing a Coq program verification project
|
|
0
|
848
|
September 5, 2020
|
|
Notation for inequality chain
|
|
4
|
1031
|
August 24, 2020
|
|
Extended simply typed lyambda calculus substitution for let term
|
|
3
|
687
|
August 20, 2020
|
|
Not a valid ring equation
|
|
3
|
932
|
August 16, 2020
|
|
Why in silly_ex (the software foundation)the first hypothesis is useless
|
|
2
|
651
|
August 16, 2020
|
|
Subtyping in Simply Typed Lambda-Calculus
|
|
5
|
911
|
August 14, 2020
|
|
Spacemacs won't let me retract the proof buffer
|
|
6
|
1374
|
August 13, 2020
|
|
Is it possible to define binary trees without a new inductive type?
|
|
1
|
1484
|
August 12, 2020
|
|
JMeq and dependent programming
|
|
4
|
1245
|
August 9, 2020
|
|
Coq Training App
|
|
1
|
622
|
August 9, 2020
|
|
Can't compile packages with coqide
|
|
1
|
682
|
August 8, 2020
|
|
Proving existence statements about coinductive types constructively
|
|
1
|
828
|
August 4, 2020
|
|
Applying hypothesis with unknown variables
|
|
1
|
592
|
July 31, 2020
|
|
Software Foundations/Logical Foundations Exercise
|
|
2
|
1084
|
July 30, 2020
|
|
Hint databases as argument
|
|
5
|
1250
|
July 27, 2020
|
|
Cbn vs simpl?
|
|
2
|
2161
|
July 23, 2020
|
|
Why Coq does not allow the containment relationship between types
|
|
3
|
1645
|
July 23, 2020
|
|
Create a definition using a proof script inside a proof script
|
|
3
|
695
|
July 21, 2020
|
|
(Finite, discrete) Probabilities in Coq?
|
|
9
|
3108
|
July 17, 2020
|
|
Nested dependent pattern matching
|
|
1
|
1312
|
July 14, 2020
|
|
Hyperlink in coqdoc
|
|
1
|
639
|
July 12, 2020
|
|
Formally verified pieces of the network stack? (eg RPC)
|
|
3
|
834
|
July 12, 2020
|
|
Tacarg in Ltac
|
|
1
|
534
|
July 10, 2020
|