|
|
|
|
|
|
by vatsachak
6 days ago
|
|
|
I don't really buy this argument because we can all read the code with the Lean LSP. Also, after using a tactic enough you can guess why it's used. Agda and Idris are more beautiful for sure, but a proof is a proof (according to the law of the excluded middle) |
|
|