Re: [mizar] Type extensions

[Freek Wiedijk <freek@cs.ru.nl>]

Dear Adam,

>Very similar problem apeared in the case of the type "Element of REAL"
>and "Element of COMPLEX" (with the earlier not extending to the latter).

Wasn't there a trick of redefining REAL to have a more
specific type, "COMPLEX_set" say, and then redefining "Element
of" when its argument is a COMPLEX_set to be a subtype of
Element of COMPLEX?  I think something like that worked for me
once.

_If_ that works it's still very clumsy, of course.  Not something
that you want.

Freek