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