[isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading
makarius at sketis.net
Tue Jan 20 18:16:43 CET 2015
On Mon, 19 Jan 2015, Jasmin Blanchette wrote:
>> Just a reminder that this old thread is not yet resolved and currently
>> I'm essentially stuck.
> I hope somebody who has a clue will answer your email.
I still have various "important" markers on this mail thread, to see if I
can tell something about it, but I did not manage to pick it up again.
It will happen really soon now ...
> I’ve applied and push your first change.
> As for semicolon, the standard style is rather to put them, not to drop
Strictly speaking there is no standard for semicolons in Isabelle/ML, only
the universal standard of uniformity: a file either has extra semicolons
or does not have extra semicolons.
More than 20 years ago, semicolons where generally en-vogue, and no
surprise for me in SML. Then they became less popular, e.g. in Scala we
now see sophisticated rules for implicit "semicolon inference". The Isar
language has lost its semicolon altogether some weeks ago (5ff61774df11).
Over the decades I have occasionally experimented with writing less
semicolons in ML, but each time I ran into practical inconveniences
concerning error situations (broken partial input), and closed ML modules
versus open sequences of declarations (e.g. in the 'ML' command).
My present style of doing it (approx. the last 10 years) is somehow
optimized in that respect. Whenever I do serious renovations on some old
ML module, I first normalize the semicolon style (and other styles as
well), just to save a lot of time in the actual work.
More information about the isabelle-dev