Re: [mizar] PVS GPLed

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

On Tue, 16 Sep 2008, Freek Wiedijk wrote:

> > Even for a (unlabeled) _tree_ there is e.g. the problem
> > of hidden arguments (a redefined functor may take some more
> > arguments on the semantic level, so there will be additional
> > edges in the tree). Or expandable vs. normal types -
> > again change already the _tree_ on the semantic level.
>
> Okay, okay, enough already!  I give in!

:-), but your insight is useful and "mostly correct"

> > And there might be some weird cases even without this,
> > e.g. when constructors with the same name are defined for
> > several arities ...
>
> I don't think that _that_ will be a problem.  The way I
> understand term syntax, this has been taken into account.

Again, mostly - here is a quick counterexample. Try uncommenting the 
commented def in following, and see how the parsing changes:

environ  vocabularies  NEWTON; begin

definition let x be set;
func choose x equals x; correctness;
func x choose equals x; correctness;
func bool x equals x; correctness;
let y be set;
func x bool y equals x; correctness;
:: func x choose y equals x; correctness;
end;

for x, y being set holds choose x bool y = x choose bool y;

Josef