Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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