Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] lattice_syntax by default?

Email Gateway (Jan 24 2023 at 16:34):

From: Fabian Huch <huch@in.tum.de>
I find it unexpected that lattice_syntax is disabled by default, as I
would consider lattices quite the canonical structure. Given that it is
pretty simple to turn the syntax back off (unbundle no_lattice_syntax),
would it make sense to have it active by default? In my experience, less
experienced users frequently stumble over that.

The counter-argument is that quite a few AFP entries (~50) define their
own symbols (mostly bottom/top), and to turn it off, one has to unbundle
the no_lattice_syntax for every import from a foreign session.

Fabian

Email Gateway (Jan 24 2023 at 20:36):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
For what it's worth, my two cents are that global notation, and global interpretations,
are inherently evil. This is much the same as my feeling about global structure definitions
in Standard ML, as opposed to functors that can be used to instantiate the structures in
the context in which they are required.

Email Gateway (Jan 25 2023 at 07:04):

From: Tobias Nipkow <nipkow@in.tum.de>
I would agree, for exactly the counter-argument Fabian gave himself.

Tobias
smime.p7s

Last updated: Apr 26 2024 at 04:17 UTC