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

Re: inductive predicates in adt



Aaron Ballard asked

> In adt theory files for datatypes, why don't the inductive predicates
> such as "subterm" need the key word, INDUCTIVE?

The INDUCTIVE keyword is needed in inductive relations *input* by users
so that the system knows to treat these definitions specially.

The definitions that appear in an _adt file are constructed internally
by PVS and the _adt file is really just an *output* representation
that serves as documentation for the user.

However, we agree that it would be clearer if these definitions did
use the keyword INDUCTIVE, and we'll consider adding it in the next
release.

John Rushby

-------