Stream: Isabelle/ML

Topic: type variable in datatype definition

view this post on Zulip HuanSun (Nov 29 2022 at 04:09):

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?

view this post on Zulip Mathias Fleury (Nov 29 2022 at 05:26):

In Isabelle you need to specify every extra type variable as a parameter of the type:

datatype 'a assn =
    ...

view this post on Zulip Mathias Fleury (Nov 29 2022 at 05:26):

And if you had more, you would have:

datatype ('a, 'b, 'c, 'd) assn =
   ...

Last updated: Dec 21 2024 at 16:20 UTC