|
|
|
|
|
|
by kmill
924 days ago
|
|
|
It's not `noncomputable` in Lean though. Lots of computable functions use it. I've read Bauer's paper before btw. I think topoi are cool, but I don't think it's a complexity worth thinking about for everyone else who isn't concerned about these things. |
|
|