|
Bug in the parser?
|
|
5
|
188
|
April 1, 2021
|
|
Not an inductive product
|
|
5
|
196
|
March 31, 2021
|
|
What axioms are built-in?
|
|
6
|
233
|
March 31, 2021
|
|
What does `auto` do differently under the hood?
|
|
1
|
182
|
March 31, 2021
|
|
Rtauto slower than tauto
|
|
0
|
150
|
March 29, 2021
|
|
How to express a list of any type X?
|
|
2
|
173
|
March 28, 2021
|
|
Solve an `exists` goal in a field with proof search?
|
|
3
|
185
|
March 26, 2021
|
|
Reasoning about higher-order program transformation?
|
|
3
|
198
|
March 26, 2021
|
|
Add LoadPath in Coq 8.12.2
|
|
5
|
308
|
March 22, 2021
|
|
Poll about proofgeneral: do you use "holes"
|
|
0
|
184
|
March 22, 2021
|
|
Defining mathematical function implicitly
|
|
4
|
181
|
March 19, 2021
|
|
Error while installing Coq platform
|
|
2
|
252
|
March 18, 2021
|
|
avoiding type error
|
|
11
|
260
|
March 11, 2021
|
|
Syntax with backticks
|
|
1
|
153
|
March 11, 2021
|
|
Equality between inductively defined relations
|
|
1
|
174
|
March 7, 2021
|
|
Parametric rewriting under binders
|
|
0
|
169
|
March 3, 2021
|
|
Contradicting instructions for installation with OPAM
|
|
2
|
201
|
March 2, 2021
|
|
Mutual Recursion with function unfolding
|
|
4
|
747
|
February 13, 2021
|
|
Application of automatic induction principle versus induction tactic
|
|
2
|
180
|
February 7, 2021
|
|
Inversion of an axiom is bad
|
|
6
|
211
|
February 6, 2021
|
|
Composing Propositions
|
|
1
|
187
|
February 2, 2021
|
|
Proving well-founded recursion using the Program module
|
|
2
|
186
|
February 1, 2021
|
|
Is there a way to prove properties about ocaml programs using a Coq verified library
|
|
2
|
239
|
January 24, 2021
|
|
Tips and tricks to make VST proof development faster
|
|
4
|
269
|
January 25, 2021
|
|
Machine learning and hammers for Coq
|
|
32
|
2584
|
January 23, 2021
|
|
Can I extract part of a module instead of the whole module?
|
|
0
|
189
|
January 20, 2021
|
|
Force application of fixpoint to its argument
|
|
11
|
253
|
January 15, 2021
|
|
What is the difference between Gallina and Ltac?
|
|
6
|
399
|
January 15, 2021
|
|
Program equivalence and substitution
|
|
3
|
191
|
January 8, 2021
|
|
Soundness of program transformation
|
|
2
|
185
|
January 7, 2021
|
