3 ms·
That depends on the ITP system. But in general, in an ITP system you can separate the name of something from how it is displayed. In the ITP system I am current
by practal 4y ago
That depends on the ITP system. But in general, in an ITP system you can separate the name of something from how it is displayed. In the ITP system I am currently building, Practal, the displayed syntax does not need to be unique. So choosing a unique name becomes simpler, because you don't have to worry so much about how it looks, because that can be entirely different and doesn't need to be unique. Apart from that, every accessible element of your mathematical universe already has a name: it is the term you use to describe it.
- beckingz 4y agoSure you can rename things easily, but NAMING something CORRECTLY is hard, in an ontological sense where you may not know what the thing's name is until you truly know what it is.
- jolux 4y agoI've never thought that "naming things" meant keeping track of the name or anything, but that's hard too. I've always thought it meant the descriptive aspect of naming.