Re: [isabelle] Notation forgets unnamed context inside type class context

Hi Andreas,

> 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.
> Moreover, I can refer to foo only via If I write "foo", this
> always gets translated to the global foo with type "('c => 'c) => 'c =>
> 'c".

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,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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