help : string -> unit

SYNOPSIS

Displays help on a given identifier in the system.

DESCRIPTION

A call help "s" will attempt to display the help file associated with a particular identifier s in the system. If there is no entry for identifier s, the call responds instead with some possibly helpful suggestions as to what you might have meant, based on a simple `edit distance' criterion. The built-in help files are stored in the Help subdirectory of HOL Light. Users can add additional locations by modifying help_path. Normally the help file for an identifier name would be called name.hlp, but there are a few exceptions, because some identifiers have characters that cannot be put in filenames and some platforms like Cygwin have inadequate case sensitivity.

FAILURE CONDITIONS

Never fails.

EXAMPLE

Here is a successful call:

  # help "lhs";;
  -------------------------------------------------------------------

  lhs : term -> term

  SYNOPSIS

  Returns the left-hand side of an equation.

  DESCRIPTION

  lhs `t1 = t2` returns `t1`.

  FAILURE CONDITIONS

  Fails with lhs if the term is not an equation.

  EXAMPLES


    # lhs `2 + 2 = 4`;;
    val it : term = `2 + 2`


  SEE ALSO
  dest_eq, lhand, rand, rhs.

  -------------------------------------------------------------------
  val it : unit = ()

and here is one for a non-existent identifier:

  # help "IMP_TAC";;
  -------------------------------------------------------------------
  No help found for "IMP_TAC"; did you mean:

  help "SIMP_TAC";;
  help "MP_TAC";;
  help "IMP_TRANS";;

  ?
  --------------------------------------------------------------------

SEE ALSO

help_path, hol_version.