[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Typechecking problem
The problem here is that in your importing, you are asking for a
set of lists of reals, so "(: 1 :)" is converted to a set of
lists by using the singleton conversion, but there is no
conversion that will work for the b assignment.
What you want is to import T1[real], and then the conversions
work as you expect.
Aditya Kanade <email@example.com> wrote:
> I'm getting a typechecking error where I atmost expect a
> TCC. Following is the scenario:
> t1:type = [# a: set[t], b:set[[(a),(a)]] #]
> end T1
> importing T1[list[real]]
> e:t1 = (# a := (: 1 :), b := (: (1,1) :) #)
> end T2
> The typechecking error is:
> Incompatible types for (: (1, 1) :)
> Found: (list_adt[[real, real]].cons?)
> Expected: sets
> [[(singleton[(cons?[real])]((: 1 :))),
> (singleton[(cons?[real])]((: 1 :)))]].set
> Now, AFAIK, PVS should have applied the list2set conversion to
> the list (: (1,1) :). I think it does that for a := (: 1 :). If I
> explicitly write list2set((: (1,1) :)), then it gives the same error,
> this time for the list2set conversion!
> At least conceptually, what I'm trying to do should work. Can anyone
> please explain the problem? And any solution to this?