1\DOC
2
3\BLTYPE
4add_infix_type : {Assoc : associativity,
5                  Name : string,
6                  ParseName : string option,
7                  Prec : int} ->
8                 unit
9\ELTYPE
10
11\SYNOPSIS
12Adds a type infix.
13
14\KEYWORDS
15Parsing, pretty-printing.
16
17\DESCRIBE
18
19A call to {add_infix_type} adds an infix type symbol to the type
20grammar.  The argument is a record of four values providing
21information about the infix.
22
23The {Assoc} field specifies the associativity of the symbol (possible
24values: {LEFT}, {RIGHT} and {NONASSOC}).  The standard HOL type
25infixes ({+}, {#}, {->} and {|->}) are all right-associative.  The
26{Name} field specifies the name of the binary type operator that is
27being mapped to.  If the name of the type is not the same as the
28concrete syntax (as in all the standard HOL examples above), the
29concrete syntax can be provided in the {ParseName} field.  The {Prec}
30field specifies the binding precedence of the infix.  This should be a
31number less than 100, and probably greater than or equal to 50, where
32the function {->} symbol lies.  The greater the number, the more
33tightly the symbol attempts to ``grab'' its arguments.
34
35\FAILURE
36Fails if the desired precedence level contains an existing infix with
37a different associativity.
38
39\EXAMPLE
40{
41- Hol_datatype `atree = Nd of 'v => ('k # atree) list`;
42<<HOL message: Defined type: "atree">>
43> val it = () : unit
44
45- add_infix_type { Assoc = LEFT, Name = "atree",
46                   ParseName = SOME ">->", Prec = 65 };
47> val it = () : unit
48
49- type_of ``Nd``;
50<<HOL message: inventing new type variable names: 'a, 'b>>
51> val it = ``:'a -> ('b # ('b >-> 'a)) list -> 'b >-> 'a`` : hol_type
52}
53
54\ENDDOC
55