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: Nov 11 2024 at 01:24 UTC