Email Gateway (Aug 18 2022 at 20:21): Email Gateway (Aug 18 2022 at 20:21):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Email Gateway (Aug 18 2022 at 20:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Last updated: Apr 26 2024 at 12:28 UTC