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