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

Recursive Type Definition


Is it possible to define a recursive (or coinductive) ``type" in PVS? I
want to define a kind of set recursively, which can be seen as:

A = { a | predicate(a,A) }

It says ``No resolution for A". How does one handle this in PVS?

-- Aditya Kanade.
Research Scholar, CSE, IIT Bombay.