----------------------------------------------------------------------
Hol_datatype                                                 (bossLib)
----------------------------------------------------------------------
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.

----------------------------------------------------------------------