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

==

Parse.== : hol_type quotation -> 'a -> hol_type

Parses a quotation into a HOL type.

An invocation ==` ... `== is identical to Type ` ... `.

Failure

As for Parse.Type.

Turns strings into types.

See also

Parse.Term