|
Various installation attempts on MacbookPro M3 Max stall or hang
|
|
4
|
258
|
January 15, 2024
|
|
Defining Mutual Induction Principles Manually
|
|
2
|
337
|
January 9, 2024
|
|
How to get rid of warnings like "Warning: Cannot open directory /usr/games/."?
|
|
8
|
269
|
January 5, 2024
|
|
Class/type hierarchies
|
|
7
|
519
|
August 28, 2023
|
|
Do multiple theorems allow the same name?
|
|
1
|
192
|
December 24, 2023
|
|
Trying a Tactic with All Visible Goals
|
|
7
|
264
|
December 22, 2023
|
|
Define inductive branch with constraint on branch parameters
|
|
1
|
179
|
December 22, 2023
|
|
Implicit argument resolution
|
|
3
|
311
|
December 22, 2023
|
|
Software foundations theorem
|
|
1
|
237
|
December 22, 2023
|
|
Generally Mapping Inequality through Unary Constructors
|
|
7
|
208
|
December 20, 2023
|
|
Newbie Question: Match Case Analysis and Propagation
|
|
4
|
243
|
December 15, 2023
|
|
The Lemma body_push in Verif_stack of VC
|
|
3
|
210
|
December 15, 2023
|
|
Using coqnative compiled files in other files
|
|
9
|
246
|
December 11, 2023
|
|
Windows installation from sources failure due to symbolic link
|
|
3
|
231
|
December 7, 2023
|
|
Modularizing Coq scripts with defining Parameters/proving Axioms
|
|
1
|
309
|
November 30, 2023
|
|
[Very basic] stack overflow and computability
|
|
1
|
381
|
November 23, 2023
|
|
Recursive definitions best practices
|
|
3
|
348
|
November 10, 2023
|
|
How to define the SEP(R) clauses?
|
|
1
|
583
|
November 8, 2023
|
|
About 'syntax error: lexer: undefined token' at the beginning
|
|
2
|
626
|
October 20, 2023
|
|
Using Bundled and Unbundled Typeclasses Simultaneously
|
|
0
|
280
|
October 18, 2023
|
|
Coqtop not found
|
|
12
|
5567
|
October 17, 2023
|
|
Ocaml native int63 extraction
|
|
0
|
384
|
October 3, 2023
|
|
CertiuCOS2
|
|
0
|
318
|
September 25, 2023
|
|
An inductive definition failed with error "Non strictly positive occurrence..."
|
|
6
|
466
|
September 22, 2023
|
|
Trouble installing coq-core on Windows
|
|
5
|
575
|
September 14, 2023
|
|
Coqtop is not running
|
|
8
|
879
|
September 8, 2023
|
|
Controlling Extraction of Specific Types
|
|
0
|
224
|
September 4, 2023
|
|
Failing when use "destruct" tactic to "or" hypothesis if the conclusion is sumbool
|
|
3
|
342
|
September 4, 2023
|
|
How to read this in-clause in the match construct?
|
|
4
|
291
|
September 1, 2023
|
|
Rewrite set equality inside a let expression
|
|
2
|
374
|
August 30, 2023
|