[isabelle] type alias mutually defined with a datatype?



The following is accepted:

 datatype exp =
   Evar nat
 | Esbst exp sbst
 and sbst = "nat => exp"

but what is the meaning of "sbst" after this definition?  E.g. the
following is not accepted:

 constdefs
   sbstid :: "sbst"
   "sbstid == %x. Evar x"

What is the story?

Thanks,
Randy







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