\DOC Hol_datatype

\TYPE {Hol_datatype : hol_type quotation -> unit}

\SYNOPSIS
Define a concrete datatype (deprecated syntax).

\KEYWORDS
type, concrete, definition.

\DESCRIBE
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
bossLib.Datatype.

\ENDDOC