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
.