|
About the Learning category
|
|
1
|
960
|
February 12, 2019
|
|
Modularizing Coq scripts with defining Parameters/proving Axioms
|
|
1
|
31
|
November 30, 2023
|
|
Windows installation from sources failure due to symbolic link
|
|
0
|
7
|
November 29, 2023
|
|
[Very basic] stack overflow and computability
|
|
1
|
53
|
November 23, 2023
|
|
Recursive definitions best practices
|
|
3
|
101
|
November 10, 2023
|
|
How to define the SEP(R) clauses?
|
|
1
|
388
|
November 8, 2023
|
|
The Lemma body_push in Verif_stack of VC
|
|
0
|
48
|
November 8, 2023
|
|
Implicit argument resolution
|
|
2
|
77
|
November 3, 2023
|
|
About 'syntax error: lexer: undefined token' at the beginning
|
|
2
|
127
|
October 20, 2023
|
|
Using Bundled and Unbundled Typeclasses Simultaneously
|
|
0
|
108
|
October 18, 2023
|
|
Coqtop not found
|
|
12
|
4254
|
October 17, 2023
|
|
Coq's equality is not Leibniz (?)
|
|
30
|
377
|
October 16, 2023
|
|
Ocaml native int63 extraction
|
|
0
|
122
|
October 3, 2023
|
|
CertiuCOS2
|
|
0
|
127
|
September 25, 2023
|
|
An inductive definition failed with error "Non strictly positive occurrence..."
|
|
6
|
143
|
September 22, 2023
|
|
Trouble installing coq-core on Windows
|
|
5
|
132
|
September 14, 2023
|
|
Coqtop is not running
|
|
8
|
163
|
September 8, 2023
|
|
Controlling Extraction of Specific Types
|
|
0
|
109
|
September 4, 2023
|
|
Failing when use "destruct" tactic to "or" hypothesis if the conclusion is sumbool
|
|
3
|
127
|
September 4, 2023
|
|
How to read this in-clause in the match construct?
|
|
4
|
119
|
September 1, 2023
|
|
Rewrite set equality inside a let expression
|
|
2
|
143
|
August 30, 2023
|
|
Class/type hierarchies
|
|
7
|
228
|
August 28, 2023
|
|
Coq official website inaccessible?
|
|
2
|
155
|
August 16, 2023
|
|
Naming inconsistency in proofs using BinInt, Zorder, and its deprecation
|
|
2
|
175
|
August 10, 2023
|
|
How does one import native cyclic integers in coq?
|
|
3
|
138
|
August 2, 2023
|
|
Name proof from Next Obligation
|
|
1
|
119
|
July 26, 2023
|
|
Automated reasoning about list permutations
|
|
2
|
225
|
July 7, 2023
|
|
Can I access Coq's way of generating readable names from inside tactics?
|
|
1
|
262
|
June 20, 2023
|
|
Extraction: adding file prefix (`open …`) & suffix (e.g. function call), from Coq or dune?
|
|
1
|
192
|
June 6, 2023
|
|
Generating depth-indexed variant of an inductive
|
|
1
|
184
|
June 16, 2023
|