3 ms·
Sure 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.
by Tainnor 6y ago
Sure 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?