3 ms·
> (But as a sidenote: couldn't you fix this with dependent types somehow?) Most proof assistants, including Lean, are built on dependent type theory.
by ogogmad 6y ago
> (But as a sidenote: couldn't you fix this with dependent types somehow?)
Most proof assistants, including Lean, are built on dependent type theory.
- Tainnor 6y agoSure but then I guess maybe you can find ergonomic improvements to your dependent type system so as not to run into the problems discussed in the article (e.g. having to reprove that something is not zero over and over again).
- OscarCunningham 6y agoMaybe the way to do that would be to prove once that x is nonzero, use that to define r = 1/x, and thereafter use multiplication by r?