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 local.foo. 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,
	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.