|
Installation attempts on MacbookPro M3 Max give Segmentation fault: 11 errors
|
|
1
|
96
|
May 22, 2024
|
|
Which library to formalise undergrad math?
|
|
2
|
115
|
May 17, 2024
|
|
Coq crashes too frequently
|
|
3
|
234
|
May 14, 2024
|
|
Using Coq to prove Lagrange's Theorem
|
|
1
|
137
|
May 12, 2024
|
|
Typeclass search with lambda in parameter
|
|
2
|
84
|
May 10, 2024
|
|
Is there a reference for using tactics in Coq so that the size of a proof is significantly reduced?
|
|
1
|
81
|
May 9, 2024
|
|
Problem with notation in CPS ceval_step extension of LF's ImpCEvalFun
|
|
2
|
99
|
May 9, 2024
|
|
Exact_no_check fails on Type
|
|
3
|
83
|
May 8, 2024
|
|
Proof if then else function with if hypothesis
|
|
4
|
295
|
May 7, 2024
|
|
Can we prove the following theorem constructively, and if not, what axioms are needed?
|
|
4
|
156
|
April 29, 2024
|
|
Is there a way to create binary floats from hexadecimals?
|
|
1
|
114
|
April 22, 2024
|
|
Replacing "true = false"
|
|
3
|
270
|
April 11, 2024
|
|
Ologs in Coq
|
|
0
|
118
|
April 10, 2024
|
|
How to simplify single-branch match expressions?
|
|
2
|
327
|
April 8, 2024
|
|
Https://coq.inria.fr/opam/released is down
|
|
3
|
127
|
April 8, 2024
|
|
How to use binary floats in Flocq
|
|
3
|
200
|
April 5, 2024
|
|
How to proof a simple statement about rational numbers
|
|
4
|
386
|
March 26, 2024
|
|
How to automatically extract anonymous subterms in a goal
|
|
0
|
142
|
March 19, 2024
|
|
Ltac with variadic argument
|
|
1
|
228
|
March 4, 2024
|
|
[Question; very basic] Stack-based virtual machine test
|
|
2
|
261
|
March 1, 2024
|
|
Destructing term when match generates equality involving that term
|
|
5
|
309
|
February 20, 2024
|
|
Negative definitions of coinductive propositions
|
|
2
|
253
|
February 19, 2024
|
|
Is constructive indefinite description a conservative extension?
|
|
4
|
271
|
February 13, 2024
|
|
Induction hypotheses, again
|
|
4
|
198
|
February 9, 2024
|
|
Coq examples of cut elimination in sequent calculi?
|
|
2
|
260
|
February 8, 2024
|
|
Simplifying/rewriting inside of an anonymous fixpoint
|
|
0
|
227
|
February 6, 2024
|
|
Dependent-typed terms as return values / function parameters
|
|
3
|
280
|
February 2, 2024
|
|
Coq platform script downloads are triggering my antivirus
|
|
4
|
222
|
January 24, 2024
|
|
Coq/Ocaml project using heuristic function written in C?
|
|
1
|
187
|
January 23, 2024
|
|
Match Case Analysis and Propagation (redux)
|
|
3
|
271
|
January 17, 2024
|