From 7a117c45bf101a8230a06110ee830f5be2de12bf Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Sat, 5 Dec 2015 10:10:59 -0800
Subject: [PATCH] feat(init/setoid): tag equivalence relation

---
 library/init/setoid.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/init/setoid.lean b/library/init/setoid.lean
index dc138dc779..3a7a00dabd 100644
--- a/library/init/setoid.lean
+++ b/library/init/setoid.lean
@@ -17,12 +17,12 @@ namespace setoid
   variable [s : setoid A]
   include s
 
-  theorem refl (a : A) : a ≈ a :=
+  theorem refl [refl] (a : A) : a ≈ a :=
   and.elim_left (@setoid.iseqv A s) a
 
-  theorem symm {a b : A} : a ≈ b → b ≈ a :=
+  theorem symm [symm] {a b : A} : a ≈ b → b ≈ a :=
   λ H, and.elim_left (and.elim_right (@setoid.iseqv A s)) a b H
 
-  theorem trans {a b c : A} : a ≈ b → b ≈ c → a ≈ c :=
+  theorem trans [trans] {a b c : A} : a ≈ b → b ≈ c → a ≈ c :=
   λ H₁ H₂, and.elim_right (and.elim_right (@setoid.iseqv A s)) a b c H₁ H₂
 end setoid