reflexivity

reflexivity solves goals which state that a term is equal to itself. reflexivity has some simplification power, but not as much as simpl. This tactic will fail if it cannot solve the goal.

reflexivity makes an attempt to simplify the goal and then apply eq_refl, where eq_refl is the sole constructor of the eq Inductive Proposition, stating that forall {A : Type} (a : A), eq a a.

Syntax

(* Simple usage *)
reflexivity.

Examples

Before

n: nat
=========================
1/1
n = n

reflexivity.

After

No more goals.

Resources

Reference Documentation

---