Email Gateway (Aug 19 2022 at 13:39): Email Gateway (Aug 19 2022 at 13:39):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
I have run into a problem with notation inside unnamed contexts in Isabelle2013-2 when the
unnamed context is nested into a type class context. Suppose that the unnamed context
fixes a parameter, locally define a constant that depends on the parameter and declare
some mixfix notation for the constant inside the unnamed context. Then, the first place
holder _ in the notation represents the parameter fixed in the unnamed context, rather
than the first parameter of the locally defined constant.
Here's an example:
theory Scratch imports Main begin
context ord begin
context fixes f :: "'b => 'b" begin
definition foo :: "'b => 'b" where "foo x = f x"
notation (input) foo ("{|_|}")
term "{|undefined :: 'b|}" -- "type error in application"
If I do the same inside a proper locale instead of the type class context, notation works
fine.
Moreover, I can refer to foo only via local.foo. If I write "foo", this always gets
translated to the global foo with type "('c => 'c) => 'c => 'c".
Is there any way to use my notation in the unnamed context?
Best,
Andreas
PS: The same trouble occurs with a recent repository version such as 601ea66c5bcd.
Email Gateway (Aug 19 2022 at 13:41):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
there is an misfit in the implementation of the class target on the one
hand side and the concept of nested context stacks on the other side:
currently, the class target assumes a »pseudo-global« situation for
definitions, which does not hold in the presence of an additional
hypothetical context.
Definitions in classes are a delicate situation (maybe you know about
the insider joke of »educated guess« now persisting since 2007 (?) in
the sources) and it is yet uncertain when this can be tackled appropriately.
All the best,
Florian
signature.asc
Last updated: Apr 26 2024 at 12:28 UTC