Re: [mizar] weak types

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

Dear Andrzej,

>with a conditional proof like
>
> sqrt x > a implies P
> proof
>  assume sqrt x > a;
>   ....
>  thus P;
> end;
>
>one gets, by default,
>
> (x >= 0 implies sqrt x > a) implies P
> proof
>  assume x >= 0 & sqrt x > a;
>   ....
>  thus P;
> end;
>
>and it seems wrong.

I see.  So I don't want to read the sqrt x > a as an
abbreviation of x >= 0 & sqrt x > a.  I just want the x >= 0
to be something that should be required to be proved before I
allow the formula sqrt x > a.

>PS. Is you paper with Ian on the Web, I would like to read it.

It's Jan, not Ian.  But yes, of course it is:
<http://www.cs.kun.nl/~freek/pubs/partial.ps.gz>.

Freek