Email Gateway (Aug 19 2022 at 11:57): Email Gateway (Aug 19 2022 at 11:57):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Dear Devs,
Users' interests should be properly represented. Users can actually
become quite interested in foundational features, and find uses for
low-level features that they are given access to. And once momentum
builds for features to be eliminated in a software product, it's can be
hard to stop, so it pays to complain early.
The quotes below from the dev list provide some context. I'll make this
a short comment, in case nothing more is required.
I care about the operator "==", and over the months, Makarius has made a
number of comments deemphasizing it, and the comments below indicate
something similar. I don't see how "==" could be gotten rid of from
Isar, but what do I know?
The operator "==" will forever be an Isar operator, won't it? It's not
going away, is it? No reply is necessary if it's not going away. I would
appreciate a reply if it's going away, so I can become irate now.
Thanks,
GB
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-September/004527.html
Last updated: Nov 21 2024 at 12:39 UTC