Re: [isabelle] Dropping global mixfix syntax



> When I declare mixfix notation with a specification command (definition,
> fun, inductive, primrec) inside an unnamed context that fixes a
> parameter, I get a warning "Dropping global mixfix syntax".
> 
> context fixes n :: nat begin
> definition foo :: nat ("myfoo") where "foo = n"
> end
> 
> I can avoid this warning if I use the notation command explicitly:
> 
> context fixes n :: nat begin
> definition foo :: nat where "foo = n"
> notation foo ("myfoo")
> end

According to my understanding of the sources, the technical difference
between both constructs is that in the first, the mixfix syntax has an
explicit representation in the local theory stack as part of the binding
and thus its non-propagation to the background theory can be reported by
the system explicitly, whereas in the latter case we have a generic
syntax declaration, which is not propagated to the background theory
since it is not »pervasive« (see files
src/Pure/Isar/(specification|local_theory|named_target|generic_target).ML).

With my current understanding, your specification is fine, and it is
doubtful about which misguided expectation the user is supposed to be
warned.  But there might be deeper reasons for this.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.