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

[PVS-Help] Record subtype from a TYPE+


Is there a way to have a record type also be a type FROM a supertype?  I
want to declare that a subtype from "values" can be interpreted as a record
type named Instructions.  But this fails:

	values TYPE+
	Instructions TYPE FROM values = [# a, b, c: int #]
Error message:
	Parser error: Found '=' when expecting 'END'


Mark Brown