Hacker News new | past | comments | ask | show | jobs | submit login

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 ?

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/IsarM...

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-...

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact