Re: [isabelle] Implicit structure argument
On Tue, 2 Apr 2013, René Neumann wrote:
Section 7.3: notation goes with a 'struct_mixfix'. (Ironically, the
nonterminal 'fixes' (p. 82) does not support "(structure)" according to
the diagram given).
The documentation is generally a bit terse, but note that formally a
syntax diagram is always an over approximation: not everything that is
syntactically correct is so semantically. The error means it is rejected
in the semantics -- there are also indirect situations where it is
rejected via low-level errors, IIRC.
I will look again if the confusion about "mixfix" and "struct_mixfix" in
the syntax can be removed, to make it just subject to semantic checking.
I can't say on the spot if it is feasible to make implicit structures
more general -- they have been a bit on retreat in recent years, and
are now a bit old-fashioned anyway.
But there is no replacement, is there?
There is no one-to-one replacement. Indexed syntax was originally
introduced as a way to make global notation usable in a local context,
with dependency on locale parameters. Later local notation and
abbreviations were introduced, and despite some challenges, they are more
powerful. This is why "(structure)" has now this old-fashioned accent
when seen in theory sources.
This archive was generated by a fusion of
Pipermail (Mailman edition) and