[isabelle] an inductive datatype and n inductively defined set

Dear all:

By my understanding, the expressbilty of an inductive datatype and an
inductively defined set in Isabelle is not the same.
An inductive datatype can be naturally corresponding to an inductively
defined set, but not vice and versa.

Who could introduce more technical papers on the relation between the two

Thanks in advance.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.