3 ms·

Isabelle allows the user to define symbols. So, those two operations are represented by different symbols in the source (the *.thy files) but the presentation l

Isabelle 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 ago
Ah, 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-...