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