improve verso docstrings

Author: datokrat

src/Init/Data/Range/Polymorphic/Basic.lean

@@ -19,16 +19,6 @@ namespace Rxc
 
 variable {α : Type u} {lo hi : α} {a : α}
 
-/--
-This typeclass provides support for the size function for ranges with closed lower bound
-({name (scope := "Init.Data.Range.Polymorphic")}`Rcc.size`,
-{name (scope := "Init.Data.Range.Polymorphic")}`Rco.size` and
-{name (scope := "Init.Data.Range.Polymorphic")}`Rci.size`).
-
-The returned size should be equal to the number of elements returned by {lit}`toList`. This
-condition is captured by the typeclass
-{name (scope := "Init.Data.Range.Polymorphic")}`LawfulRangeSize`.
--/
 class HasSize (α : Type u) where
   /-- Returns the number of elements starting from {name}`lo` that satisfy the given upper bound. -/
   size (lo hi : α) : Nat
@@ -54,6 +44,18 @@ class LawfulHasSize (α : Type u) [LE α] [UpwardEnumerable α] [HasSize α] whe
       (h' : UpwardEnumerable.succ? lo = some lo') :
       HasSize.size lo hi = HasSize.size lo' hi + 1
 
+/--
+This typeclass provides support for the size function for ranges with closed lower bound
+({name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rcc.size`,
+{name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rco.size` and
+{name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rci.size`).
+
+The returned size should be equal to the number of elements returned by {lit}`toList`. This
+condition is captured by the typeclass
+{name}`LawfulHasSize`.
+-/
+add_decl_doc HasSize
+
 export LawfulHasSize (size_eq_zero_of_not_le size_eq_one_of_succ?_eq_none
   size_eq_succ_of_succ?_eq_some)
 
@@ -92,16 +94,6 @@ namespace Rxo
 
 variable {α : Type u} {lo hi : α} {a : α}
 
-/--
-This typeclass provides support for the size function for ranges with open lower bound
-({name (scope := "Init.Data.Range.Polymorphic")}`Roc.size`,
-{name (scope := "Init.Data.Range.Polymorphic")}`Roo.size` and
-{name (scope := "Init.Data.Range.Polymorphic")}`Roi.size`).
-
-The returned size should be equal to the number of elements returned by {lit}`toList`. This
-condition is captured by the typeclass
-{name (scope := "Init.Data.Range.Polymorphic")}`LawfulRangeSize`.
--/
 class HasSize (α : Type u) where
   /-- Returns the number of elements starting from {name}`lo` that satisfy the given upper bound. -/
   size (lo hi : α) : Nat
@@ -127,6 +119,18 @@ class LawfulHasSize (α : Type u) [LT α] [UpwardEnumerable α] [HasSize α] whe
       (h' : UpwardEnumerable.succ? lo = some lo') :
       HasSize.size lo hi = HasSize.size lo' hi + 1
 
+/--
+This typeclass provides support for the size function for ranges with open lower bound
+({name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Roc.size`,
+{name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Roo.size` and
+{name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Roi.size`).
+
+The returned size should be equal to the number of elements returned by {lit}`toList`. This
+condition is captured by the typeclass
+{name}`LawfulHasSize`.
+-/
+add_decl_doc HasSize
+
 export LawfulHasSize (size_eq_zero_of_not_le size_eq_one_of_succ?_eq_none
   size_eq_succ_of_succ?_eq_some)
 
@@ -165,16 +169,6 @@ namespace Rxi
 
 variable {α : Type u} {lo : α} {a : α}
 
-/--
-This typeclass provides support for the size function for ranges with closed lower bound
-({name (scope := "Init.Data.Range.Polymorphic")}`Ric.size`,
-{name (scope := "Init.Data.Range.Polymorphic")}`Rio.size` and
-{name (scope := "Init.Data.Range.Polymorphic")}`Rii.size`).
-
-The returned size should be equal to the number of elements returned by {lit}`toList`. This
-condition is captured by the typeclass
-{name (scope := "Init.Data.Range.Polymorphic")}`LawfulRangeSize`.
--/
 class HasSize (α : Type u) where
   /-- Returns the number of elements starting from {name}`lo` that satisfy the given upper bound. -/
   size (lo : α) : Nat
@@ -197,6 +191,18 @@ class LawfulHasSize (α : Type u) [UpwardEnumerable α] [HasSize α] where
       (h : UpwardEnumerable.succ? lo = some lo') :
       HasSize.size lo = HasSize.size lo' + 1
 
+/--
+This typeclass provides support for the size function for ranges with closed lower bound
+({name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Ric.size`,
+{name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rio.size` and
+{name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rii.size`).
+
+The returned size should be equal to the number of elements returned by {lit}`toList`. This
+condition is captured by the typeclass
+{name}`LawfulHasSize`.
+-/
+add_decl_doc HasSize
+
 export LawfulHasSize (size_eq_one_of_succ?_eq_none size_eq_succ_of_succ?_eq_some)
 
 theorem size_pos {α : Type u} [UpwardEnumerable α] [HasSize α] [LawfulHasSize α] {lo : α} :

src/Init/Data/Range/Polymorphic/Instances.lean

@@ -90,12 +90,6 @@ end Rxc
 
 namespace Rxo
 
--- TODO: Replace the `lit` role with an intra-module forward reference.
-/--
-Creates a {lean}`HasSize α` from a {lean}`HasSize α` instance. If the latter is lawful
-and certain other conditions hold, then the former is also lawful by
-{lit}`Rxo.LawfulHasSize.open_of_closed`.
--/
 @[inline]
 abbrev HasSize.ofClosed [Rxc.HasSize α] : HasSize α where
   size lo hi := Rxc.HasSize.size lo hi - 1
@@ -138,6 +132,13 @@ instance LawfulHasSize.of_closed [UpwardEnumerable α] [LE α] [DecidableLE α]
       refine ⟨h.choose, ?_⟩
       simpa [succMany?_succ?_eq_succ?_bind_succMany?, h'] using h.choose_spec
 
+/--
+Creates a {lean}`HasSize α` from a {lean}`HasSize α` instance. If the latter is lawful
+and certain other conditions hold, then the former is also lawful by
+{name}`Rxo.LawfulHasSize.of_closed`.
+-/
+add_decl_doc HasSize.ofClosed
+
 instance instIsAlwaysFiniteOfLawfulHasSize [LT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [HasSize α] [LawfulHasSize α] :
     IsAlwaysFinite α where