[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] access n-th argument of a function?



Hello,

I am curious if there is in the PVS syntax, a way to access the n-th argument of a function by its index, something like 

F(a1,a2,a3,a4,a5,a6,... : posnat) :posnat  = args(3)

where args(3) would be a3. 

what I am actually trying to do is to convert a function with a big number of arguments into a map:

F(a1,a2,a3,a4:posnat) = lambda ( i : below(n) ) : if i=1 then a1 else if i=2 then a2 else if i=3 then a3....

but it seems very impractical using if-functions.

Thanks in advance,

Romain Jobredeaux