Mike Shulman

I like the idea of it displaying only textual ranges and treating other types of locations as "no location", but I'm not sure how that would work in practice without...

I guess I could see either of those working. If you feel like trying to implement something here (which I don't think you need to), maybe pick whatever seems best/easiest...

It might also be useful for locations to mix textual and non-textual information. For example, a component of a graphical proof might include a text box where the user can...

Sounds good!

Yeah, I wouldn't expect Asai to munge messages supplied by the programmer. That's their own lookout. Basically I want to be able to change this line: https://github.com/RedPRL/asai/blob/main/src/tty/Tty.ml#L66 I don't know...

Hmm, perhaps the intent was for part (ii) to say something like "$f(x)\neq 0$ if and only if $x \\# 0$"? Then it ought to be equivalent to analytic LPO,...

I think my suggested change would keep the intended punch.

"max" is only used for the real numbers or other ordered field, not for an arbitrary lattice, and these orders are linear. In classical mathematics, any supremum in a linear...

I think it's more than just a least upper bound. The classical condition $\mathrm{max}(x,y) \in \\{x,y\\}$ is equivalent to $(\mathrm{max}(x,y) = x) \vee (\mathrm{max}(x,y) = y)$, so when rephrasing this...

> the general rule for “constructivizing” classical math concepts is to go for the strongest notion that makes useful sense. I don't think that "strongest" is always quite the right...