|
|
|
|
|
|
by mcguire
2832 days ago
|
|
|
Imagine having to prove a Coq theorem for every function call. No, it's not really that bad. But almost. I really suggest you play with Idris some; what you can do with it is brilliant, for simple tasks. For complicated tasks, like the fully general propositions you need for library functions, it can get much more complicated than the code itself. |
|
|