Re: [mizar] weak types

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

Hi Josef,

>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?

Freek