op --> : hol_type * hol_type -> hol_type
STRUCTURE
Type
SYNOPSIS
Right associative infix operator for building a function type.
DESCRIPTION
If ty1 and ty2 are HOL types, then ty1 --> ty2 builds the HOL type ty1 -> ty2.
FAILURE
Never fails.
EXAMPLE
- bool --> alpha;
> val it = `:bool -> 'a` : hol_type

COMMENTS
This operator associates to the right, that is, ty1 --> ty2 --> ty3 is identical to ty1 --> (ty2 --> ty3).
SEEALSO
dom_rng, mk_type, mk_thy_type
HOL  Trindemossen-1