1\DOC 2 3\TYPE {thytype_abbrev : {Name:string,Thy:string} * hol_type * bool -> unit} 4 5\SYNOPSIS 6Abbreviates a type to a specific theory-qualified name. 7 8\KEYWORDS 9Parsing, pretty-printing. 10 11\DESCRIBE 12A call to {thytype_abbrev({Name=n,Thy=t}, ty, prp)} establishes the 13``kernel'' name {t$n} as an abbreviation for the type {ty}, as happens 14with {type_abbrev}. The boolean flag {prp} indicates whether or not 15this abbreviation will also be used when the printer comes to print 16the given type. In other words, after the call it becomes possible to 17write {``:args t$n``} to stand for type {ty}. If there are type 18variables in {ty} they become the parameters to the new abbreviated 19type operator. These parameters need to be filled in in the {args} 20position above. If there are no type variables in {ty} then 21abbreviation is of a whole type, and {args} must be blank. 22 23If there was an existing abbreviation for {t$n}, then this will be 24replaced by the call. 25 26In addition, after the given call, this abbreviation will become the 27preferred binding for the bare name {n}. Other abbreviations in 28different theories will need to use the form with fully-qualified 29names ({thy1$n}, {thy2$n} etc). 30 31If the boolean flag is false, this invocation is comparable to the 32behaviour after {intputonly_type_abbrev}: the abbreviation can be used 33to input types of the desired pattern, but such types will print as 34they did previously. 35 36\FAILURE 37Fails if {ty} is a variable type. 38 39\COMMENTS 40As with other parsing and pretty-printing functions, there is a 41companion function, {temp_thytype_abbrev}, which has the same effect 42on the global grammar but does not cause the change to persist when 43the theory is exported. 44 45It is legitimate to use a string for the theory component of the 46record that does not correspond to the current theory. Indeed, it is 47perfectly reasonable to do this, if one wants to give priority to a 48particular ancestral abbreviation. 49 50\SEEALSO 51Parse.type_abbrev. 52 53\ENDDOC 54