|
Unable to use the induction hypothesis in In_map_iff
|
|
3
|
90
|
July 1, 2024
|
|
Unable to correctly use the 'apply' tactic
|
|
3
|
97
|
June 28, 2024
|
|
Issue with syntax in tr_rev_correct
|
|
2
|
82
|
June 27, 2024
|
|
How to destruct H involving two variables
|
|
2
|
142
|
June 27, 2024
|
|
Suppressing Repeated Warnings from "Disable Notation" Command in Coq
|
|
4
|
213
|
June 25, 2024
|
|
"Not bound variables at all" but also can't find and instance
|
|
4
|
101
|
June 25, 2024
|
|
Proving obvious logic
|
|
3
|
263
|
June 21, 2024
|
|
How to prove a function is uniquely specified?
|
|
3
|
113
|
June 21, 2024
|
|
A Couple of Questions Regarding Building Projects with Dune
|
|
2
|
213
|
June 17, 2024
|
|
Making use of a definition inside a proof
|
|
4
|
192
|
June 5, 2024
|
|
Rewrite variable value in hypothesis
|
|
1
|
189
|
June 3, 2024
|
|
Polymorphic seq
|
|
1
|
97
|
May 24, 2024
|
|
Strange failure of general rewriting
|
|
0
|
94
|
May 24, 2024
|
|
Strange failure in typeclass resolution
|
|
2
|
134
|
May 22, 2024
|
|
Installation attempts on MacbookPro M3 Max give Segmentation fault: 11 errors
|
|
1
|
109
|
May 22, 2024
|
|
Which library to formalise undergrad math?
|
|
2
|
141
|
May 17, 2024
|
|
Coq crashes too frequently
|
|
3
|
343
|
May 14, 2024
|
|
Using Coq to prove Lagrange's Theorem
|
|
1
|
167
|
May 12, 2024
|
|
Typeclass search with lambda in parameter
|
|
2
|
99
|
May 10, 2024
|
|
Is there a reference for using tactics in Coq so that the size of a proof is significantly reduced?
|
|
1
|
105
|
May 9, 2024
|
|
Problem with notation in CPS ceval_step extension of LF's ImpCEvalFun
|
|
2
|
123
|
May 9, 2024
|
|
Exact_no_check fails on Type
|
|
3
|
109
|
May 8, 2024
|
|
Proof if then else function with if hypothesis
|
|
4
|
488
|
May 7, 2024
|
|
Can we prove the following theorem constructively, and if not, what axioms are needed?
|
|
4
|
208
|
April 29, 2024
|
|
Is there a way to create binary floats from hexadecimals?
|
|
1
|
129
|
April 22, 2024
|
|
Replacing "true = false"
|
|
3
|
337
|
April 11, 2024
|
|
Ologs in Coq
|
|
0
|
138
|
April 10, 2024
|
|
How to simplify single-branch match expressions?
|
|
2
|
401
|
April 8, 2024
|
|
Https://coq.inria.fr/opam/released is down
|
|
3
|
180
|
April 8, 2024
|
|
How to use binary floats in Flocq
|
|
3
|
258
|
April 5, 2024
|