[isabelle-dev] typrep?

[Florian Haftmann]

Hi Amine,

I guess you are in the following thygraph situation:

    Typrep  Real
       | /  \ |
       |/    \|
Complex_Main  FPS
       \      /
        \    /
         \  /
          Foo

Real defines type real, Typerep class typerep (;-)).  Then both in
Complex_Main and FPS and instance for typerep on type real is generated
automatically (thanks to generic interpretation), which clash on merge
into theory Foo.

The solution is too arrange that there is only one meeting point of
Typrep and Real in the thygraph.  According to your second email you
have already found a way.

N.B. arranging the HOL thygraph is a nontrivial task!

Cheers,
	Florian

Amine Chaieb schrieb:
> This behaviour is even more strange than I thought.
>=20
>=20
> I am trying to merge my theory with Complex_Main . The latter looks lik=
e:
>=20
>=20
> theory Complex_Main
>=20
> imports
>   Main
>   Real
>   Fundamental_Theorem_Algebra
>   Log
>   Ln
>   Taylor
>   Integration
>   FrechetDeriv
> begin
>=20
> end
>=20
>=20
> Now when I merge my theory with all the theories imorted by
> Complex_Main, it works. Is this behaviour really intended? Maybe I
> should reboot?
>=20
>=20
> Best wishes,
>=20
> Amine.
>=20
>=20
> Amine Chaieb wrote:
>=20
>> Dear all,
>>
>> When I try to merge two theories I get this (to me new) error message:=

>>
>>
>> *** Clash of specifications
>> "Complex_Main.typerep_real_inst.typerep_real_def" and
>> "FPS.typerep_real_inst.typerep_real_def" for constant
>> "Typerep.typerep_class.typerep"
>>
>> *** At command "theory".
>>
>>
>>
>> What does it mean? I do not mention typerep, nor typerep_real, no real=

>> at all. I guess it has something to do with the typedef package, but
>> what is it?
>>
>>
>> Any hint is welcome.
>>
>> Best wishes,
>>
>> Amine.
>>
>> _______________________________________________
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabell=
e-dev
>>  =20
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle=
-dev

--=20

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_in=
formatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090120/362dc67f/attachment.sig>