[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
features.

Thanks in advance.

lyj




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