[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

Is there any reason why I should not use mixfix syntax with specifications in such contexts?

Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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