max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: add missing docstrings for Rxy.Sliceable (#11472)

Browse source 
This PR adds missing docstrings for the `mkSlice` methods.
This commit is contained in:
David Thrane Christiansen 2025-12-02 09:42:36 +01:00 • committed by GitHub
parent 3dd99fc29c
commit 0e83422fb6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 28 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/Init/Data/Slice/Notation.lean
View file

@ -9,6 +9,7 @@ prelude
public import Init.Data.Range.Polymorphic.PRange
set_option doc.verso true
set_option linter.missingDocs true
public section
@ -30,6 +31,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Rcc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` to {lean}`range.upper`, both inclusive.
-/
mkSlice (carrier : α) (range : Rcc β) : γ
/--
@ -39,6 +43,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of resulting the slices is {lit}`γ`.
-/
class Rco.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` (inclusive) to {lean}`range.upper` (exclusive).
-/
mkSlice (carrier : α) (range : Rco β) : γ
/--
@ -48,6 +55,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Rci.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` (inclusive).
-/
mkSlice (carrier : α) (range : Rci β) : γ
/--
@ -57,6 +67,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Roc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` (exclusive) to {lean}`range.upper` (inclusive).
-/
mkSlice (carrier : α) (range : Roc β) : γ
/--
@ -66,6 +79,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Roo.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` to {lean}`range.upper`, both exclusive.
-/
mkSlice (carrier : α) (range : Roo β) : γ
/--
@ -75,6 +91,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Roi.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` (exclusive).
-/
mkSlice (carrier : α) (range : Roi β) : γ
/--
@ -84,6 +103,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Ric.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` up to {lean}`range.upper` (inclusive).
-/
mkSlice (carrier : α) (range : Ric β) : γ
/--
@ -93,6 +115,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Rio.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` up to {lean}`range.upper` (exclusive).
-/
mkSlice (carrier : α) (range : Rio β) : γ
/--
@ -102,6 +127,9 @@ index type {lit}`β`.
The type of the resulting slices is {lit}`γ`.
-/
class Rii.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` with no bounds.
-/
mkSlice (carrier : α) (range : Rii β) : γ
macro_rules