Re: [mizar] Assumption in redefinition?

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

Hi,

Mizar does not allow assumptions in redefinitions. You can write it, but
you cannot refer to it. To have a requested result type you should put it
into the original definition. Or you can substitute permissive definition
by new one where you indicate a value of the functor in "nonsense" case.
(see for example REAL_1:def 2. I do not want to say that this
definition has no sense).

Artur


On Sun, 5 Jan 2003, Freek Wiedijk wrote:

> Dear Adam,
>
> >Can you provide a more elaborate context ?
>
> It was a redefinition to give it a more specific type...
>
> Freek
>