4 ms·
> couldn't you fix this with dependent types somehow? quoting from the post: > the way I had set things up, every time I used the [sqrt] symbol I had to suppl
by uryga 6y ago
> couldn't you fix this with dependent types somehow?
quoting from the post:
> the way I had set things up, every time I used the [sqrt] symbol I had to supply a proof that what I was taking the square root of was non-negative.
"supplying a proof" is how you do it in dependently-typed systems afaik. the author tried it, and it was inconvenient