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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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