|
|
|
|
|
|
by vjerancrnjak
359 days ago
|
|
|
Thing with "classes" is that you need to identify them before proving and you need to prove the implication to general case. Lean is not powerful enough to do this, to somehow conclude that there's a finite set of cases on which you can run brute-force checks and prove a general case. |
|
|