Comment by smj-edison
5 days ago
I've heard this can be a bit of a pain in practice, is that true? I can imagine it could slow me down to construct a proof of an invariant every time I call a function (if I understand correctly).
5 days ago
I've heard this can be a bit of a pain in practice, is that true? I can imagine it could slow me down to construct a proof of an invariant every time I call a function (if I understand correctly).
I haven't worked significantly with lean but I'm toying with my own dependently typed language. generally you only have to construct a proof once, much like a type or function, and then you reuse it. Also, depending on the language there are rewriting semantics ("elaboration") that let you do mathematical transformations to make two statements equivalent and then reuse the standardized proof.