|
About the Learning category
|
|
1
|
368
|
February 12, 2019
|
|
Parametric rewriting under binders
|
|
0
|
19
|
March 3, 2021
|
|
Contradicting instructions for installation with OPAM
|
|
2
|
72
|
March 2, 2021
|
|
Extraction to Haskell Int type
|
|
1
|
38
|
March 1, 2021
|
|
What axioms are built-in?
|
|
5
|
55
|
February 25, 2021
|
|
Mutual Recursion with function unfolding
|
|
4
|
426
|
February 13, 2021
|
|
Add LoadPath in Coq 8.12.2
|
|
2
|
57
|
February 12, 2021
|
|
Application of automatic induction principle versus induction tactic
|
|
2
|
75
|
February 7, 2021
|
|
Inversion of an axiom is bad
|
|
6
|
84
|
February 6, 2021
|
|
Composing Propositions
|
|
1
|
65
|
February 2, 2021
|
|
Proving well-founded recursion using the Program module
|
|
2
|
82
|
February 1, 2021
|
|
Is there a way to prove properties about ocaml programs using a Coq verified library
|
|
2
|
120
|
January 24, 2021
|
|
Tips and tricks to make VST proof development faster
|
|
4
|
126
|
January 25, 2021
|
|
Machine learning and hammers for Coq
|
|
32
|
2168
|
January 23, 2021
|
|
Can I extract part of a module instead of the whole module?
|
|
0
|
76
|
January 20, 2021
|
|
Force application of fixpoint to its argument
|
|
11
|
115
|
January 15, 2021
|
|
What is the difference between Gallina and Ltac?
|
|
6
|
146
|
January 15, 2021
|
|
avoiding type error
|
|
10
|
125
|
January 14, 2021
|
|
Program equivalence and substitution
|
|
3
|
70
|
January 8, 2021
|
|
Soundness of program transformation
|
|
2
|
76
|
January 7, 2021
|
|
Using CoqGym on my own files
|
|
3
|
132
|
January 7, 2021
|
|
Fomalisation of Bell and Lapadula model
|
|
1
|
81
|
December 30, 2020
|
|
naming existentials
|
|
2
|
80
|
December 30, 2020
|
|
instantiating existentials
|
|
3
|
82
|
December 29, 2020
|
|
Convert ident to string in ltac
|
|
2
|
142
|
December 16, 2020
|
|
How to avoid awkward assertions
|
|
2
|
101
|
December 11, 2020
|
|
Dependent Pair Injectivity equivalent to K
|
|
4
|
145
|
November 20, 2020
|
|
Smart Matches
|
|
3
|
140
|
November 12, 2020
|
|
Trying to prove sort algorithm correctness (for specific n), in search for hints
|
|
11
|
217
|
October 20, 2020
|
|
Bug in universe inference?
|
|
3
|
144
|
October 27, 2020
|
