mk_const : string * (hol_type * hol_type) list -> term

SYNOPSIS

Produce constant term by applying an instantiation to its generic type.

DESCRIPTION

This is the basic way of constructing a constant term in HOL Light, applying a specific instantiation (by type_subst) to its generic type. It may sometimes be more convenient to use mk_mconst, which just takes the desired type for the constant and finds the instantiation itself; that is also a natural inverse for dest_const. However, mk_const is likely to be significantly faster.

FAILURE CONDITIONS

Fails if there is no constant of the given type.

EXAMPLE

  # get_const_type "=";;
  val it : hol_type = `:A->A->bool`

  # mk_const("=",[`:num`,`:A`]);;
  val it : term = `(=)`
  # type_of it;;
  val it : hol_type = `:num->num->bool`

  # mk_const("=",[`:num`,`:A`]) = mk_mconst("=",`:num->num->bool`);;
  val it : bool = true