1\DOC Hol_datatype
2
3\TYPE {Hol_datatype : hol_type quotation -> unit}
4
5\SYNOPSIS
6Define a concrete datatype (deprecated syntax).
7
8\KEYWORDS
9type, concrete, definition.
10
11\DESCRIBE
12The {Hol_datatype} function provides exactly the same definitional
13power as the {Datatype} function (which see), with a slightly
14different input syntax, given below:
15{
16   spec    ::= [ <binding> ; ]* <binding>
17
18   binding ::= <ident> = [ <clause> | ]* <clause>
19            |  <ident> = <| [ <ident> : <type> ; ]* <ident> : <type> |>
20
21   clause  ::= <ident>
22            |  <ident> of [<type> => ]* <type>
23}
24
25\EXAMPLE
26For example, what with {Datatype} would be
27{
28   Datatype`btree = Leaf 'a | Node btree 'b btree
29}
30is
31{
32   Hol_datatype `btree = Leaf of 'a
33                       | Node of btree => 'b => btree`
34}
35when using {Hol_datatype}.
36
37The {=>} notation in the description highlights the fact that, in HOL,
38constructors are by default curried.
39
40\COMMENTS
41The {Datatype} function's syntax is easier to write and easier to understand.
42
43\SEEALSO
44bossLib.Datatype.
45
46\ENDDOC
47