[isabelle] the itself type constructor
Using the repository version of Isabelle, and working in HOL, I find I
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and