Re: [mizar] weak types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Fri, 21 Nov 2003, Freek Wiedijk wrote:

> >The idea is, that for types T1 < T2 (e.g. non-zero complex < complex), you 
> >give those terms formally typed as T2 "the benefit of doubt", i.e. if you 
> >need T1 for them instead, you temporarily use a formal casting (retract) 
> >operator, and delay the verification of T1 until "run-time".
> 
> This is like "reconsider" on the term level?  So you don't
> need to give the "reconsidered" expression a new name like in
> Mizar?

Yes, it is related to "reconsider", but only works downwards, and 
automatically. I think this would be still too strong for Mizar, I would 
suggest to have some finer mechanisms for this, e.g. only try it for some 
functors or some types, where it is useful.
Other difference is, that for "reconsider",  you can provide arbitrary 
justification, which would be quite unwanted in such cases. So this would 
now have sense, only in cases when the checker is strong enough to prove 
the typing directly from the type definition. Other solution is in 
allowing some special purpose "tactics" (yes I know how unpopular this 
word is :-) for such reductions, like are the elements of computer algebra 
already now.