Hol_datatype : hol_type quotation -> unit
STRUCTURE
SYNOPSIS
Define a concrete datatype (deprecated syntax).
DESCRIPTION
The Hol_datatype function provides exactly the same definitional power as the Datatype function (which see), with a slightly different input syntax, given below:
   spec    ::= [ <binding> ; ]* <binding>

   binding ::= <ident> = [ <clause> | ]* <clause>
            |  <ident> = <| [ <ident> : <type> ; ]* <ident> : <type> |>

   clause  ::= <ident>
            |  <ident> of [<type> => ]* <type>
EXAMPLE
For example, what with Datatype would be
   Datatype`btree = Leaf 'a | Node btree 'b btree
is
   Hol_datatype `btree = Leaf of 'a
                       | Node of btree => 'b => btree`
when using Hol_datatype.

The => notation in the description highlights the fact that, in HOL, constructors are by default curried.

COMMENTS
The Datatype function’s syntax is easier to write and easier to understand.
SEEALSO
HOL  Kananaskis-13