-->
op Type.--> : hol_type * hol_type -> hol_type
Right associative infix operator for building a function type.
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 -> α”: hol_type
Comments
This operator associates to the right, that is, ty1 --> ty2 --> ty3 is
identical to ty1 --> (ty2 --> ty3).