REFL : term -> thm

SYNOPSIS

Returns theorem expressing reflexivity of equality.

DESCRIPTION

REFL maps any term `t` to the corresponding theorem |- t = t.

FAILURE CONDITIONS

Never fails.

EXAMPLE

  # REFL `2`;;
  val it : thm = |- 2 = 2

  # REFL `p:bool`;;
  val it : thm = |- p <=> p

COMMENTS

This is one of HOL Light's 10 primitive inference rules.

SEE ALSO

ALL_CONV, REFL_TAC.