Re: [mizar] Type extensions

[Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>]

Artur Kornilowicz wrote:

> On Wed, 13 Sep 2006, Andrzej Trybulec wrote:
>
> > Dear Adam,
> >
> > I appreciate what Josef wrote, but it is rather about the extension 
> > of Mizar, and I guess you asked what to do now. Without revision 
> > nothing can be done, I think. So, the definition must be repeated.
> >
> > The solution, that I like, is to use 'real-valued' and 
> > 'ext-real-valued' attributes (it is now 'real-yielding', I think  
> > that 'real-valued' is better name, have anybody an opinion about 
> > it?). Then instead of  'PartFunc of X,REAL' we should use 
> > 'real-valued ManySortedSet of X'.
>
>
>
>
> ManySortedSet is total, so we need a similar type to represent PartFunc.
Right, my mistake. I have observed the need of such 'partial manysorted 
set' earlier. So, I think we have to introduce such a type. How to call 
it? I would rather avoid 'many sorted' in the name.

Regards,
Andrzej