parse_type : string -> hol_type

SYNOPSIS

Parses a string into a HOL type.

DESCRIPTION

The call parse_type "s" parses the string s into a HOL type. This is the function that is invoked automatically when a type is written in quotations with an initial colon `:s`.

FAILURE CONDITIONS

Fails in the event of a syntax error or unparsed input.

EXAMPLE

  # parse_type "num->bool";;
  val it : hol_type = `:num->bool`

SEE ALSO

lex, parse_term.