type variable in datatype definition

Question

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?

Answer 1

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.