add a comment about coercion

leanprover-community · Oct 9, 2024 · 0b2bd17 · 0b2bd17
1 parent 59d91a1
commit 0b2bd17
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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 })