From 89e860ac8bd8000f798b7ede2b32fd3dfd22dfe8 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Fri, 30 Jun 2017 05:16:42 -0400
Subject: [PATCH] doc(init/core): Document init_quotient in lean

This way people can search for "constant quot" and find it in the lean source. Plus the init_quotient command only occurs once, so this way people know what it means.
---
 library/init/core.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/library/init/core.lean b/library/init/core.lean
index 0e12aa03d8..d39c6f0060 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -120,6 +120,19 @@ prefix `¬` := not
 inductive eq {α : Sort u} (a : α) : α → Prop
 | refl : eq a
 
+/-
+Initialize the quotient module, which effectively adds the following definitions:
+
+constant quot {α : Sort u} (r : α → α → Prop) : Sort u
+
+constant quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : quot r
+
+constant quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
+  (∀ a b : α, r a b → eq (f a) (f b)) → quot r → β
+
+constant quot.ind {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} :
+  (∀ a : α, β (quot.mk r a)) → ∀ q : quot r, β q
+-/
 init_quotient
 
 inductive heq {α : Sort u} (a : α) : Π {β : Sort u}, β → Prop