Re: PVS GPLed

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