[isabelle] the itself type constructor



Using the repository version of Isabelle, and working in HOL, I find I
can't write

   datatype 'a atyp_tag = aword "'a itself" | aptr_tt

It gives me the strangest error too.   If I write "option" instead of
"itself" it works.  If I write "foo" instead of "itself" it gives me
an error because foo is not a recognised constructor.   But with
"itself", I get 

*** Illegal type for constant "op =" :: 'a itself => 'a itself => bool
*** At command "datatype".

Should my declaration work?

Michael.







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