type_of

Term.type_of : term -> hol_type

Returns the type of a term.

Failure

Never fails.

Example

> type_of boolSyntax.universal;
val it = “:(α -> bool) -> bool”: hol_type