PAULSON , Lawrence

In the process of describing systems and their properties, users of proof assistants introduce not only recursive datatypes, but also sets constructed by a recursive process. These sets are often represented by their characteristic predicates, and we use the terms interchangeably. Such sets or predicates are said to be inductively defined and...