Re: [isabelle] type alias mutually defined with a datatype?
The following is accepted:
datatype exp =
| 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