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 like
Aex "('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?
In Isabelle you need to specify every extra type variable as a parameter of the type:
datatype 'a assn = ...
And if you had more, you would have:
datatype ('a, 'b, 'c, 'd) assn = ...
Last updated: Dec 07 2023 at 16:21 UTC