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

[PVS-Help] Datatype with dependent type for constructor arguments



Hi all

I want to define a generic datatype with some constructors having argument of a dependent type

Foo[T:TYPE] DATATYPE
BEGIN
	new(list:list[T]):new?
	add(self:Foo, index:nat) : add?
END Foo

I want to constraint "index" : {i:nat | 0 <= i <= length(list)}
But this does not work because of context, "list" is unknown for "add"
I tried several ideas but unfortunately I did not find the good solution.

Any idea is welcome.
Thanks

Jean-Claude.Royer@mines-nantes.fr
ASCOLA, Mines de Nantes - INRIA
+ 33 2 51 85 82 05