doc: doc-strings to module docs in Data/Array/Lemmas (#6144)
This PR converts 3 doc-string to module docs since it seems that this is what they were intended to be!
This commit is contained in:
parent
b894464191
commit
56a80dec1b
1 changed files with 3 additions and 3 deletions
|
|
@ -621,7 +621,7 @@ theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
|
|||
(ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
|
||||
simp [getElem?_def]
|
||||
|
||||
/-- # mkArray -/
|
||||
/-! # mkArray -/
|
||||
|
||||
@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
|
||||
List.length_replicate ..
|
||||
|
|
@ -637,7 +637,7 @@ theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
|
|||
(mkArray n v)[i]? = if i < n then some v else none := by
|
||||
simp [getElem?_def]
|
||||
|
||||
/-- # mem -/
|
||||
/-! # mem -/
|
||||
|
||||
@[simp] theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
|
||||
|
||||
|
|
@ -659,7 +659,7 @@ theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
|
|||
(x ∈ if p then l else #[]) ↔ p ∧ x ∈ l := by
|
||||
split <;> simp_all
|
||||
|
||||
/-- # get lemmas -/
|
||||
/-! # get lemmas -/
|
||||
|
||||
theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} (_ : a[idx] = x) :
|
||||
idx < a.size :=
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue