I want to modify the datatype which is now defined as below.
datatype assn =
Aemp (*r Empty heap *)
| Apointsto exp exp (infixl "⟼" 200) (*r Singleton heap *)
| Astar assn assn (infixl "**" 100) (*r Separating conjunction *)
| Awand assn assn (*r Separating implication *)
| Apure bexp (*r Pure assertion *)
| Aconj assn assn (*r Conjunction *)
| Adisj assn assn (*r Disjunction *)
| Aex "(nat ⇒ assn)" (*r Existential quantification *)
I want to modify the last line to allow a more flexible existence definition, something likeAex "('a ⇒ assn)", however, the ide notice me with the error message Extra type variables on right-hand side: "'a" . By the way, I can write Aex (A: Type) (pp: A -> assn). in Coq. Therefore, I wonder wether I can do it in Isabelle and how?
For the sake of putting the answer here too: In Isabelle you have to specify what the dependencies of the types. Therefore, you need to write:
datatype 'a assn =
...
And if you had several ones, you would write:
datatype ('a, 'b, 'c, 'd) assn =
...
Remark that the error message "Extra XXX on the right-hand side" means there is something on the right-hand side that is missing from the left-hand side of the equality. Depending on the context, this could be some extra variable, some extra type (like here), or anything else.