dom_rng

Type.dom_rng : hol_type -> hol_type * hol_type

Breaks a function type into domain and range types.

If ty has the form ty1 -> ty2, then dom_rng ty yields (ty1,ty2).

Failure

Fails if ty is not a function type.

Example

> dom_rng (bool --> alpha);
val it = (“:bool”, “:α”): hol_type * hol_type

> try dom_rng bool;
Exception- HOL_ERR (at Type.dom_rng: not a function type) raised

See also

Type.-->, Type.dest_type, Type.dest_thy_type