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

[PVS-Help] function domains



Is it possible to extract the domain of a function?  Eg, given 

f: [T1 -> T2] = ...

the expression f`domain returns the set T1.  Similarly for

f: [{t: T1 | p(t)} -> T2] = ...

the expression f`domain returns the set {t: T1 | p(t)}.  

Thanks,
Rob