|
Destructing term when match generates equality involving that term
|
|
5
|
390
|
February 20, 2024
|
|
Negative definitions of coinductive propositions
|
|
2
|
286
|
February 19, 2024
|
|
Is constructive indefinite description a conservative extension?
|
|
4
|
418
|
February 13, 2024
|
|
Induction hypotheses, again
|
|
4
|
248
|
February 9, 2024
|
|
Coq examples of cut elimination in sequent calculi?
|
|
2
|
287
|
February 8, 2024
|
|
Simplifying/rewriting inside of an anonymous fixpoint
|
|
0
|
249
|
February 6, 2024
|
|
Dependent-typed terms as return values / function parameters
|
|
3
|
312
|
February 2, 2024
|
|
Coq platform script downloads are triggering my antivirus
|
|
4
|
253
|
January 24, 2024
|
|
Coq/Ocaml project using heuristic function written in C?
|
|
1
|
205
|
January 23, 2024
|
|
Match Case Analysis and Propagation (redux)
|
|
3
|
353
|
January 17, 2024
|
|
Various installation attempts on MacbookPro M3 Max stall or hang
|
|
4
|
286
|
January 15, 2024
|
|
Defining Mutual Induction Principles Manually
|
|
2
|
423
|
January 9, 2024
|
|
How to get rid of warnings like "Warning: Cannot open directory /usr/games/."?
|
|
8
|
351
|
January 5, 2024
|
|
Class/type hierarchies
|
|
7
|
589
|
August 28, 2023
|
|
Do multiple theorems allow the same name?
|
|
1
|
199
|
December 24, 2023
|
|
Trying a Tactic with All Visible Goals
|
|
7
|
319
|
December 22, 2023
|
|
Define inductive branch with constraint on branch parameters
|
|
1
|
192
|
December 22, 2023
|
|
Implicit argument resolution
|
|
3
|
345
|
December 22, 2023
|
|
Software foundations theorem
|
|
1
|
261
|
December 22, 2023
|
|
Generally Mapping Inequality through Unary Constructors
|
|
7
|
267
|
December 20, 2023
|
|
Newbie Question: Match Case Analysis and Propagation
|
|
4
|
281
|
December 15, 2023
|
|
The Lemma body_push in Verif_stack of VC
|
|
3
|
238
|
December 15, 2023
|
|
Using coqnative compiled files in other files
|
|
9
|
298
|
December 11, 2023
|
|
Windows installation from sources failure due to symbolic link
|
|
3
|
264
|
December 7, 2023
|
|
Modularizing Coq scripts with defining Parameters/proving Axioms
|
|
1
|
343
|
November 30, 2023
|
|
[Very basic] stack overflow and computability
|
|
1
|
413
|
November 23, 2023
|
|
Recursive definitions best practices
|
|
3
|
395
|
November 10, 2023
|
|
How to define the SEP(R) clauses?
|
|
1
|
594
|
November 8, 2023
|
|
About 'syntax error: lexer: undefined token' at the beginning
|
|
2
|
703
|
October 20, 2023
|
|
Using Bundled and Unbundled Typeclasses Simultaneously
|
|
0
|
303
|
October 18, 2023
|