[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
schropp at in.tum.de
Fri Aug 26 22:27:51 CEST 2011
On 08/26/2011 10:50 PM, Brian Huffman wrote:
> On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp<schropp at in.tum.de> wrote:
>> On 08/26/2011 10:38 PM, Makarius wrote:
>>> What is gained from that apart from having two versions of typedef?
>> I am with you here.
>> We don't need two primitive versions of typedefs.
> This is incorrect: Only the predicate-based typedef need be primitive.
> The set-based typedef can be implemented definitionally as a thin
> layer on top of the predicate-based one.
That is exactly what I said below the quoted line. ;>
I guess this discussion only came about because you said HOL4-style
typedefs, which cannot be used as the primitive.
> - Brian
More information about the isabelle-dev