lint(order/lexographic, pilex): docstrings (#4489)

Docstrings in `order/lexographic` and `order/pilex`
leanprover-community · Oct 7, 2020 · 2e77ef6 · 2e77ef6
1 parent afffab1
commit 2e77ef6
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/src/order/lexicographic.lean b/src/order/lexicographic.lean
@@ -10,6 +10,7 @@ import tactic.basic
 
 universes u v
 
+/-- The cartesian product, equipped with the lexicographic order. -/
 def lex (α : Type u) (β : Type v) := α × β
 
 variables {α : Type u} {β : Type v}

diff --git a/src/order/pilex.lean b/src/order/pilex.lean
@@ -10,9 +10,12 @@ import algebra.order_functions
 variables {ι : Type*} {β : ι → Type*} (r : ι → ι → Prop)
   (s : Π {i}, β i → β i → Prop)
 
+/-- The lexicographic relation on `Π i : ι, β i`, where `ι` is ordered by `r`,
+  and each `β i` is ordered by `s`. -/
 def pi.lex (x y : Π i, β i) : Prop :=
 ∃ i, (∀ j, r j i → x j = y j) ∧ s (x i) (y i)
 
+/-- The cartesian product of an indexed family, equipped with the lexicographic order. -/
 def pilex (α : Type*) (β : α → Type*) : Type* := Π a, β a
 
 instance [has_lt ι] [∀ a, has_lt (β a)] : has_lt (pilex ι β) :=