|
About the Learning category
|
|
1
|
380
|
February 12, 2019
|
|
Apparently bad installation of coq (im a newbie)
|
|
0
|
6
|
April 10, 2021
|
|
Turning "exists unique" into a function in Coq
|
|
3
|
98
|
April 3, 2021
|
|
Bug in the parser?
|
|
5
|
57
|
April 1, 2021
|
|
Not an inductive product
|
|
5
|
66
|
March 31, 2021
|
|
What axioms are built-in?
|
|
6
|
103
|
March 31, 2021
|
|
What does `auto` do differently under the hood?
|
|
1
|
45
|
March 31, 2021
|
|
Rtauto slower than tauto
|
|
0
|
30
|
March 29, 2021
|
|
How to express a list of any type X?
|
|
2
|
56
|
March 28, 2021
|
|
Solve an `exists` goal in a field with proof search?
|
|
3
|
51
|
March 26, 2021
|
|
Reasoning about higher-order program transformation?
|
|
3
|
76
|
March 26, 2021
|
|
Add LoadPath in Coq 8.12.2
|
|
5
|
105
|
March 22, 2021
|
|
Poll about proofgeneral: do you use "holes"
|
|
0
|
63
|
March 22, 2021
|
|
Defining mathematical function implicitly
|
|
4
|
76
|
March 19, 2021
|
|
Error while installing Coq platform
|
|
2
|
52
|
March 18, 2021
|
|
avoiding type error
|
|
11
|
155
|
March 11, 2021
|
|
Syntax with backticks
|
|
1
|
55
|
March 11, 2021
|
|
Equality between inductively defined relations
|
|
1
|
65
|
March 7, 2021
|
|
Parametric rewriting under binders
|
|
0
|
54
|
March 3, 2021
|
|
Contradicting instructions for installation with OPAM
|
|
2
|
90
|
March 2, 2021
|
|
Extraction to Haskell Int type
|
|
1
|
60
|
March 1, 2021
|
|
Mutual Recursion with function unfolding
|
|
4
|
486
|
February 13, 2021
|
|
Application of automatic induction principle versus induction tactic
|
|
2
|
84
|
February 7, 2021
|
|
Inversion of an axiom is bad
|
|
6
|
104
|
February 6, 2021
|
|
Composing Propositions
|
|
1
|
78
|
February 2, 2021
|
|
Proving well-founded recursion using the Program module
|
|
2
|
92
|
February 1, 2021
|
|
Is there a way to prove properties about ocaml programs using a Coq verified library
|
|
2
|
131
|
January 24, 2021
|
|
Tips and tricks to make VST proof development faster
|
|
4
|
139
|
January 25, 2021
|
|
Machine learning and hammers for Coq
|
|
32
|
2277
|
January 23, 2021
|
|
Can I extract part of a module instead of the whole module?
|
|
0
|
84
|
January 20, 2021
|
