Re: [isabelle] type alias mutually defined with a datatype?


The following is accepted:

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

... but it is not what one would expect. You have defined a unit datatype with the single constructor called "nat => exp". :-)

I am not sure if there is a way to refer to the constructor later, but you can see that it exists:

lemma "(x::sbst) = y)"
apply (cases x)

goal (1 subgoal):
 1. x = nat => exp ==> x = y

However, such definitions should probably not be allowed...


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