8 ms·
If it can be done, it needs to be done at the presentation layer, I guess so too. It has been a while since I worked with Isabelle locales. So how come that in
by auggierose 7y ago
If it can be done, it needs to be done at the presentation layer, I guess so too.
It has been a while since I worked with Isabelle locales. So how come that in your example "x + y" is not being confused with "A + B", although all involved entities are ZF sets? Or does A actually have a different type than x ?
- robinzfc 7y agoIsabelle allows the user to define symbols. So, those two operations are represented by different symbols in the source (the *.thy files) but the presentation layer renders them both as "+". You may want to look at the corresponding IsarMathLib source at [1] on GitHub. Isabelle/ZF uses only two types: set ("i") and prop("o"). [1] https://github.com/SKolodynski/IsarMathLib/blob/master/IsarMathLib/TopologicalGroup_ZF.thy https://github.com/SKolodynski/IsarMathLib/blob/master/IsarM...
- auggierose 7y agoAh, I see. So, when I type in those formulas, can I use + or do I need to type in the original symbols? Nevermind, I know the answer to that. That's why Set theory notation is a difficult problem, and you need some sort of type presentation / input layer. Some people also refer to that as a user space type system or soft types: https://www21.in.tum.de/~krauss/publication/2010-soft-types-note/ https://www21.in.tum.de/~krauss/publication/2010-soft-types-...