Re: If A=B & (A contains C), why mizar doesn't infer (B contains C)

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

Yes, what I meant is probably what you call fictitious argument. The
general case I thought about is when the argument does not occur in the
definition.

There is practically no sense in having fictitious variables in loci (I
can think of a very hypothetical case, when e.g. the type "Element of X"
is needed, but we don't care at all about X (it is fictitious)).
But once we have them, why not handle them the same way as superfluous
variables in redefinitions, or at least warn the user (or both)? 

I think the real problem is understanding hidden variables. It is a nice
feature to have them, and not to have to mention all of the "implicit
context" in the notation, but it may be confusing when one is learning
Mizar. Maybe adding the possibility to view items in the inner cnstructors
notation (e.g. as in Grzegorz's Encyclopedia) would help this.
 
Josef

On Fri, 22 Jun 2001, Andrzej Trybulec wrote:

> 
> 
> Josef Urban wrote:
> 
> > I think it is a good idea, to require that the checker would accept
> > such inferences. There are some mechanisms in the checker that almost do
> > this, e.g. if you first defined
> 
> > I think it would not be too difficult to implement this "forgetting of
> > hidden arguments" in general case, not just for redefinitions.
> >
> 
> You cannot just forget the hidden arguments. You may forget fictitious
> arguments, it does not matter if they are hidden or visible. But if the
> argument is ficitious, then why to have it among loci of the definition.
> 
> I believe it is important point: if we make the system even a bit more
> complicated, it must be useful
> 
> Andrzej
>