From 0b2bd171d0edb798017e44fc19f45f2844f1e42c Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Wed, 9 Oct 2024 20:19:41 +0800
Subject: [PATCH] add a comment about coercion

---
 Mathlib/Data/Quot.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean
index 09cdc6aa8b7d2..3ea8919f38fde 100644
--- a/Mathlib/Data/Quot.lean
+++ b/Mathlib/Data/Quot.lean
@@ -21,6 +21,7 @@ variable {α : Sort*} {β : Sort*}
 
 namespace Setoid
 
+-- Pretty print `@Setoid.r _ s a b` as `s a b`.
 run_cmd Lean.Elab.Command.liftTermElabM do
   Lean.Meta.registerCoercion ``Setoid.r
     (some { numArgs := 2, coercee := 1, type := .coeFun })