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

[PVS-Help] D_infinity construction in PVS




In PVS, is it possible to construct a sequence type D, where D(0) is
some given type, and D(n+1) has type [D(n) -> D(n)].  This is used in
Scott's D_infinity construction.

Thanks,

Steven.