Re: [mizar] weak types

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

> If you have x >= 0 & sqrt x > a you have sqrt x > a and then
> you certainly have x >= 0 implies sqrt x > a, right?  So you
> can apply the implication to the assumption then?

I do not understand. Let me repeat more carefully the reason that we dropped
the &/implies approach:
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. So, could you explain what did you mean?

Andrzej

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

AT