[Hol-info] Datatype definition in HOL4

[Magnus M. <mag...@cl...>]

Hi,

Is it possible to define the following datatype in HOL4?

  exp =
    Var of num
  | App of exp # exp
  | Abs of (num -> exp)

When the above is given to HOL_datatype, it responds:

   Can't find definition for nested type: fun

(This datatype comes from Adam Chlipala's Coq paper at POPL'10.)

Thanks,
Magnus