Re: [mizar] Assumption in redefinition?

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Freek,

On Sat, 4 Jan 2003, Freek Wiedijk wrote:

>   define
>    let k,d being Nat;
>    assume
>   A1: k <= d;
>    redefine func foo(k,d) ...
>    ...
>   end;
>
> Then Mizar tells me I may not use this assumption A1.  But
> "foo" only is meaningful when k <= d!  So what can I do?

I cannot reproduce your error...
I've just tried:

environ
begin

definition
let x,y be set;
pred x < y means not contradiction;
end;

definition
let x,y be set;
assume x < y;
func x + y means not contradiction;
correctness;
::>       *4
end;

definition
let x,y be set;
assume A1: x < y;
redefine func x + y means not contradiction;
correctness by A1;
::>          *4
end;
::>
::> 4: This inference is not accepted

and this is just as expected. Can you provide a more elaborate context ?

Adam Naumowicz