add test file from Std

src/Init/Tactics.lean

@@ -369,6 +369,14 @@ macro "rfl" : tactic => `(tactic| eq_refl)
 
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 
+/--
+This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
+relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
+-/
+syntax (name := applyRfl) "apply_rfl" : tactic
+
+macro_rules | `(tactic| rfl) => `(tactic| apply_rfl)
+
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).

src/Lean/Elab/Tactic/Rfl.lean

@@ -23,4 +23,9 @@ relation, that is, a relation which has a reflexive lemma tagged with the attrib
 elab_rules : tactic
   | `(tactic| rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
 
+@[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl : Tactic := fun stx =>
+  match stx with
+  | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.Rfl

tests/lean/run/refl.lean

@@ -0,0 +1,35 @@
+set_option linter.missingDocs false
+
+example (a : Nat) : a = a := rfl
+
+example (a : Nat) : a = a := by rfl
+
+open Setoid
+
+universe u
+variable {α : Sort u} [Setoid α]
+
+@[refl] def iseqv_refl (a : α) : a ≈ a :=
+  iseqv.refl a
+
+example (a : α) : a ≈ a := by rfl
+
+example (a : Nat) : a ≤ a := by (fail_if_success rfl); apply Nat.le_refl
+
+attribute [refl] Nat.le_refl
+
+example (a : Nat) : a ≤ a := by rfl
+
+structure Foo
+
+def Foo.le (_ _ : Foo) := Unit → True
+instance : LE Foo := ⟨Foo.le⟩
+
+@[refl] theorem Foo.le_refl (a : Foo) : a ≤ a := fun _ => trivial
+
+example (a : Foo) : a ≤ a := by apply Foo.le_refl
+example (a : Foo) : a ≤ a := by rfl
+
+example (x : Nat) : x ≤ x := by
+  show _
+  rfl