|
Inversion of an axiom is bad
|
|
6
|
926
|
February 6, 2021
|
|
Composing Propositions
|
|
1
|
772
|
February 2, 2021
|
|
Proving well-founded recursion using the Program module
|
|
2
|
626
|
February 1, 2021
|
|
Is there a way to prove properties about ocaml programs using a Coq verified library
|
|
2
|
903
|
January 24, 2021
|
|
Tips and tricks to make VST proof development faster
|
|
4
|
1087
|
January 25, 2021
|
|
Can I extract part of a module instead of the whole module?
|
|
0
|
579
|
January 20, 2021
|
|
Force application of fixpoint to its argument
|
|
11
|
2039
|
January 15, 2021
|
|
What is the difference between Gallina and Ltac?
|
|
6
|
3077
|
January 15, 2021
|
|
Program equivalence and substitution
|
|
3
|
866
|
January 8, 2021
|
|
Soundness of program transformation
|
|
2
|
668
|
January 7, 2021
|
|
Using CoqGym on my own files
|
|
3
|
882
|
January 7, 2021
|
|
Fomalisation of Bell and Lapadula model
|
|
1
|
597
|
December 30, 2020
|
|
naming existentials
|
|
2
|
1040
|
December 30, 2020
|
|
instantiating existentials
|
|
3
|
1832
|
December 29, 2020
|
|
Convert ident to string in ltac
|
|
2
|
1130
|
December 16, 2020
|
|
How to avoid awkward assertions
|
|
2
|
727
|
December 11, 2020
|
|
Dependent Pair Injectivity equivalent to K
|
|
4
|
1149
|
November 20, 2020
|
|
Smart Matches
|
|
3
|
639
|
November 12, 2020
|
|
Trying to prove sort algorithm correctness (for specific n), in search for hints
|
|
11
|
1265
|
October 20, 2020
|
|
Bug in universe inference?
|
|
3
|
775
|
October 27, 2020
|
|
Stuck at Multiset.v contents_cons_inv
|
|
1
|
618
|
October 25, 2020
|
|
Why induction principle such as list_rect cannot be added in Hint database?
|
|
2
|
642
|
October 21, 2020
|
|
Tool for drawing coq project dependency graph?
|
|
15
|
2033
|
October 14, 2020
|
|
Inserting PPX annotations into extracted OCaml
|
|
2
|
832
|
October 12, 2020
|
|
Pattern matching: warn unused parameter?
|
|
1
|
804
|
October 10, 2020
|
|
What determines whether a custom entry is used for printing?
|
|
5
|
1066
|
October 6, 2020
|
|
PHOAS encoding of pattern matching notations
|
|
6
|
932
|
October 5, 2020
|
|
Definitional equalities for universal properties?
|
|
2
|
663
|
October 4, 2020
|
|
How to utilize extensionality when rewriting
|
|
4
|
1185
|
October 4, 2020
|
|
How can I use destruct given the constraint I have for index range of a list?
|
|
1
|
563
|
October 4, 2020
|