Re: [isabelle] Duplicate constant declaration in sublocale



Hi Lars,

> I have locale A, B and I want to declare B as a sublocale of A. In doing
> so, some of the constants in A can be replaced by simpler ones. I tried
> to use the same names first, but got the following error from the
> sublocale command:
> 
>   Duplicate constant declaration "local.g" vs. "local.g"
> 
> This is not to surprising. However, if I change the definition of g in B
> by removing the explicit type annotation (or use some other type
> variable there), the sublocale command succeeds (of course, this is not
> a solution to my problem, because I want to have exactly the specified
> type for my constant).

I have no concrete idea, but I guess this is due to the pitfalls of
parsing and processing those interpretation expressions, as Clemens has
indicated on a similar thread on isabelle-dev.

Cheers,
	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.