Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

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.