Loogle!

Result

Found 7159 declarations mentioning Array. Of these, only the first 200 are shown.

Array 📋 Init.Prelude
(α : Type u) : Type u
Array.empty 📋 Init.Prelude
{α : Type u} : Array α
Array.mkArray0 📋 Init.Prelude
{α : Type u} : Array α
ByteArray.data 📋 Init.Prelude
(self : ByteArray) : Array UInt8
ByteArray.mk 📋 Init.Prelude
(data : Array UInt8) : ByteArray
Lean.Syntax.getArgs 📋 Init.Prelude
(stx : Lean.Syntax) : Array Lean.Syntax
Array.mkArray1 📋 Init.Prelude
{α : Type u} (a₁ : α) : Array α
Array.emptyWithCapacity 📋 Init.Prelude
{α : Type u} (c : ℕ) : Array α
Array.mkEmpty 📋 Init.Prelude
{α : Type u} (c : ℕ) : Array α
Array.size 📋 Init.Prelude
{α : Type u} (a : Array α) : ℕ
Array.mk 📋 Init.Prelude
{α : Type u} (toList : List α) : Array α
Array.mkArray2 📋 Init.Prelude
{α : Type u} (a₁ a₂ : α) : Array α
Array.toList 📋 Init.Prelude
{α : Type u} (self : Array α) : List α
List.toArray 📋 Init.Prelude
{α : Type u_1} (xs : List α) : Array α
Lean.Syntax.node 📋 Init.Prelude
(info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax) : Lean.Syntax
Lean.TSyntaxArray.mk 📋 Init.Prelude
{ks : Lean.SyntaxNodeKinds} (as : Array Lean.Syntax) : Lean.TSyntaxArray ks
Lean.TSyntaxArray.mkImpl 📋 Init.Prelude
{ks : Lean.SyntaxNodeKinds} : Array Lean.Syntax → Lean.TSyntaxArray ks
Lean.TSyntaxArray.raw 📋 Init.Prelude
{ks : Lean.SyntaxNodeKinds} (as : Lean.TSyntaxArray ks) : Array Lean.Syntax
Lean.TSyntaxArray.rawImpl 📋 Init.Prelude
{ks : Lean.SyntaxNodeKinds} : Lean.TSyntaxArray ks → Array Lean.Syntax
Lean.Syntax.SepArray.elemsAndSeps 📋 Init.Prelude
{sep : String} (self : Lean.Syntax.SepArray sep) : Array Lean.Syntax
Lean.Syntax.SepArray.mk 📋 Init.Prelude
{sep : String} (elemsAndSeps : Array Lean.Syntax) : Lean.Syntax.SepArray sep
Array.getD 📋 Init.Prelude
{α : Type u_1} (a : Array α) (i : ℕ) (v₀ : α) : α
Array.mkArray3 📋 Init.Prelude
{α : Type u} (a₁ a₂ a₃ : α) : Array α
Array.push 📋 Init.Prelude
{α : Type u} (a : Array α) (v : α) : Array α
Lean.mkNullNode 📋 Init.Prelude
(args : Array Lean.Syntax := #[]) : Lean.Syntax
Array.appendCore 📋 Init.Prelude
{α : Type u} (as bs : Array α) : Array α
Array.mkArray4 📋 Init.Prelude
{α : Type u} (a₁ a₂ a₃ a₄ : α) : Array α
Lean.Syntax.TSepArray.elemsAndSeps 📋 Init.Prelude
{ks : Lean.SyntaxNodeKinds} {sep : String} (self : Lean.Syntax.TSepArray ks sep) : Array Lean.Syntax
Lean.Syntax.TSepArray.mk 📋 Init.Prelude
{ks : Lean.SyntaxNodeKinds} {sep : String} (elemsAndSeps : Array Lean.Syntax) : Lean.Syntax.TSepArray ks sep
Array.mkArray5 📋 Init.Prelude
{α : Type u} (a₁ a₂ a₃ a₄ a₅ : α) : Array α
Array.get!Internal 📋 Init.Prelude
{α : Type u} [Inhabited α] (a : Array α) (i : ℕ) : α
Array.get!InternalBorrowed 📋 Init.Prelude
{α : Type u} [Inhabited α] (a : Array α) (i : ℕ) : α
Array.mkArray6 📋 Init.Prelude
{α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ : α) : Array α
Lean.mkNode 📋 Init.Prelude
(k : Lean.SyntaxNodeKind) (args : Array Lean.Syntax) : Lean.TSyntax k
Array.appendCore.loop 📋 Init.Prelude
{α : Type u} (bs : Array α) (i j : ℕ) (as : Array α) : Array α
Array.extract.loop 📋 Init.Prelude
{α : Type u_1} (as : Array α) (i j : ℕ) (bs : Array α) : Array α
Array.mkArray7 📋 Init.Prelude
{α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ : α) : Array α
Array.mkArray8 📋 Init.Prelude
{α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : α) : Array α
Array.getInternal 📋 Init.Prelude
{α : Type u} (a : Array α) (i : ℕ) (h : i < a.size) : α
Array.getInternalBorrowed 📋 Init.Prelude
{α : Type u} (a : Array α) (i : ℕ) (h : i < a.size) : α
Array.extract 📋 Init.Prelude
{α : Type u_1} (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : Array α
ForIn.toArray 📋 Init.Control.Id
{ρ : Type u_1} {α : Type u} [inst : ForIn Id ρ α] (xs : ρ) : Array α
Option.toArray 📋 Init.Data.Option.Basic
{α : Type u_1} : Option α → Array α
ByteArray.ext 📋 Init.Data.ByteArray.Bootstrap
{x y : ByteArray} : x.data = y.data → x = y
ByteArray.data_push 📋 Init.Data.ByteArray.Bootstrap
{a : ByteArray} {b : UInt8} : (a.push b).data = a.data.push b
Lean.Module.commands 📋 Init.MetaTypes
(self : Lean.Module) : Array Lean.Syntax
Lean.Module.mk 📋 Init.MetaTypes
(header : Lean.Syntax) (commands : Array Lean.Syntax) : Lean.Module
Array.instGetElem?NatLtSize 📋 Init.GetElem
{α : Type u_1} : GetElem? (Array α) ℕ α fun xs i => i < xs.size
Array.instGetElemNatLtSize 📋 Init.GetElem
{α : Type u_1} : GetElem (Array α) ℕ α fun xs i => i < xs.size
Array.instLawfulGetElemNatLtSize 📋 Init.GetElem
{α : Type u_1} : LawfulGetElem (Array α) ℕ α fun xs i => i < xs.size
Array.get!Internal_eq_getElem! 📋 Init.GetElem
{α : Type u_1} [Inhabited α] (a : Array α) (i : ℕ) : a.get!Internal i = a[i]!
Array.getInternal_eq_getElem 📋 Init.GetElem
{α : Type u_1} (a : Array α) (i : ℕ) (h : i < a.size) : a.getInternal i h = a[i]
List.toArrayImpl 📋 Init.Data.List.ToArrayImpl
{α : Type u_1} (xs : List α) : Array α
List.toArrayAux 📋 Init.Data.List.ToArrayImpl
{α : Type u_1} : List α → Array α → Array α
Array.setIfInBounds 📋 Init.Data.Array.Set
{α : Type u_1} (xs : Array α) (i : ℕ) (v : α) : Array α
Array.set! 📋 Init.Data.Array.Set
{α : Type u_1} (xs : Array α) (i : ℕ) (v : α) : Array α
Array.set 📋 Init.Data.Array.Set
{α : Type u_1} (xs : Array α) (i : ℕ) (v : α) (h : i < xs.size := by get_elem_tactic) : Array α
Array.instFunctor 📋 Init.Data.Array.Basic
: Functor Array
Array.range 📋 Init.Data.Array.Basic
(n : ℕ) : Array ℕ
Array.instAppend 📋 Init.Data.Array.Basic
{α : Type u} : Append (Array α)
Array.instEmptyCollection 📋 Init.Data.Array.Basic
{α : Type u} : EmptyCollection (Array α)
Array.instInhabited 📋 Init.Data.Array.Basic
{α : Type u} : Inhabited (Array α)
Array.isEmpty 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) : Bool
Array.singleton 📋 Init.Data.Array.Basic
{α : Type u} (v : α) : Array α
Array.usize 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) : USize
Array.Mem 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (a : α) : Prop
Array.back? 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) : Option α
Array.getEvenElems 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) : Array α
Array.instMembership 📋 Init.Data.Array.Basic
{α : Type u} : Membership α (Array α)
Array.pop 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) : Array α
Array.replicate 📋 Init.Data.Array.Basic
{α : Type u} (n : ℕ) (v : α) : Array α
Array.reverse 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) : Array α
Array.toListImpl 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) : List α
Array.allDiff 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (as : Array α) : Bool
Array.back! 📋 Init.Data.Array.Basic
{α : Type u} [Inhabited α] (xs : Array α) : α
Array.countP 📋 Init.Data.Array.Basic
{α : Type u} (p : α → Bool) (as : Array α) : ℕ
Array.drop 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : ℕ) : Array α
Array.eraseIdx! 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : ℕ) : Array α
Array.eraseIdxIfInBounds 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : ℕ) : Array α
Array.findIdx 📋 Init.Data.Array.Basic
{α : Type u} (p : α → Bool) (as : Array α) : ℕ
Array.flatten 📋 Init.Data.Array.Basic
{α : Type u} (xss : Array (Array α)) : Array α
Array.instBEq 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] : BEq (Array α)
Array.instLE 📋 Init.Data.Array.Basic
{α : Type u} [LT α] : LE (Array α)
Array.instLT 📋 Init.Data.Array.Basic
{α : Type u} [LT α] : LT (Array α)
Array.instRepr 📋 Init.Data.Array.Basic
{α : Type u} [Repr α] : Repr (Array α)
Array.reduceOption 📋 Init.Data.Array.Basic
{α : Type u} (as : Array (Option α)) : Array α
Array.repr 📋 Init.Data.Array.Basic
{α : Type u} [Repr α] (xs : Array α) : Std.Format
Array.shrink 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (n : ℕ) : Array α
Array.take 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : ℕ) : Array α
Array.append 📋 Init.Data.Array.Basic
{α : Type u} (as bs : Array α) : Array α
Array.appendList 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (bs : List α) : Array α
Array.contains 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (as : Array α) (a : α) : Bool
Array.count 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (a : α) (as : Array α) : ℕ
Array.elem 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (a : α) (as : Array α) : Bool
Array.eraseP 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (p : α → Bool) : Array α
Array.eraseReps 📋 Init.Data.Array.Basic
{α : Type u_1} [BEq α] (as : Array α) : Array α
Array.find? 📋 Init.Data.Array.Basic
{α : Type u} (p : α → Bool) (as : Array α) : Option α
Array.findIdx? 📋 Init.Data.Array.Basic
{α : Type u} (p : α → Bool) (as : Array α) : Option ℕ
Array.findRev? 📋 Init.Data.Array.Basic
{α : Type} (p : α → Bool) (as : Array α) : Option α
Array.idxOf 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (a : α) : Array α → ℕ
Array.insertIdx! 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (i : ℕ) (a : α) : Array α
Array.insertIdxIfInBounds 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (i : ℕ) (a : α) : Array α
Array.leftpad 📋 Init.Data.Array.Basic
{α : Type u} (n : ℕ) (a : α) (xs : Array α) : Array α
Array.ofFn 📋 Init.Data.Array.Basic
{α : Type u} {n : ℕ} (f : Fin n → α) : Array α
Array.popWhile 📋 Init.Data.Array.Basic
{α : Type u} (p : α → Bool) (as : Array α) : Array α
Array.rightpad 📋 Init.Data.Array.Basic
{α : Type u} (n : ℕ) (a : α) (xs : Array α) : Array α
Array.takeWhile 📋 Init.Data.Array.Basic
{α : Type u} (p : α → Bool) (as : Array α) : Array α
Array.toListAppend 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (l : List α) : List α
Array.erase 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (as : Array α) (a : α) : Array α
Array.getMax? 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (lt : α → α → Bool) : Option α
Array.idxOf? 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (xs : Array α) (v : α) : Option ℕ
Array.instHAppendList 📋 Init.Data.Array.Basic
{α : Type u} : HAppend (Array α) (List α) (Array α)
Array.isPrefixOf 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (as bs : Array α) : Bool
Array.map 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β
Array.modify 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : ℕ) (f : α → α) : Array α
Array.modifyOp 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (idx : ℕ) (f : α → α) : Array α
Array.sum 📋 Init.Data.Array.Basic
{α : Type u_1} [Add α] [Zero α] : Array α → α
Array.swapIfInBounds 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i j : ℕ) : Array α
Array.findIdx?.loop 📋 Init.Data.Array.Basic
{α : Type u} (p : α → Bool) (as : Array α) (j : ℕ) : Option ℕ
Array.findSome? 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β
Array.findSomeRev? 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β
Array.flatMap 📋 Init.Data.Array.Basic
{α : Type u} {β : Type u_1} (f : α → Array β) (as : Array α) : Array β
Array.isEqv 📋 Init.Data.Array.Basic
{α : Type u} (xs ys : Array α) (p : α → α → Bool) : Bool
Array.mapIdx 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} (f : ℕ → α → β) (as : Array α) : Array β
Array.replace 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (xs : Array α) (a b : α) : Array α
Array.swapAt! 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : ℕ) (v : α) : α × Array α
Array.findFinIdx? 📋 Init.Data.Array.Basic
{α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size)
Array.findSome! 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} [Inhabited β] (f : α → Option β) (xs : Array α) : β
Array.instForMOfMonad 📋 Init.Data.Array.Basic
{α : Type u} {m : Type u_1 → Type u_2} [Monad m] : ForM m (Array α) α
Array.partition 📋 Init.Data.Array.Basic
{α : Type u} (p : α → Bool) (as : Array α) : Array α × Array α
Array.zip 📋 Init.Data.Array.Basic
{α : Type u} {β : Type u_1} (as : Array α) (bs : Array β) : Array (α × β)
Array.reverse.loop 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (i : ℕ) (j : Fin as.size) : Array α
Array.finIdxOf? 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (xs : Array α) (v : α) : Option (Fin xs.size)
Array.range' 📋 Init.Data.Array.Basic
(start size : ℕ) (step : ℕ := 1) : Array ℕ
Array.unzip 📋 Init.Data.Array.Basic
{α : Type u} {β : Type u_1} (as : Array (α × β)) : Array α × Array β
Array.idxOfAux 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (xs : Array α) (v : α) (i : ℕ) : Option (Fin xs.size)
Array.toArray_toList 📋 Init.Data.Array.Basic
{α : Type u} {xs : Array α} : xs.toList.toArray = xs
Array.zipWith 📋 Init.Data.Array.Basic
{α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (as : Array α) (bs : Array β) : Array γ
Array.emptyWithCapacity_eq 📋 Init.Data.Array.Basic
{α : Type u_1} {n : ℕ} : Array.emptyWithCapacity n = #[]
Array.mkEmpty_eq 📋 Init.Data.Array.Basic
{α : Type u_1} {n : ℕ} : Array.mkEmpty n = #[]
Array.findIdxM? 📋 Init.Data.Array.Basic
{α : Type u} {m : Type → Type u_1} [Monad m] (p : α → m Bool) (as : Array α) : m (Option ℕ)
Array.findM? 📋 Init.Data.Array.Basic
{m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α)
Array.findRevM? 📋 Init.Data.Array.Basic
{α : Type} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α)
Array.firstM 📋 Init.Data.Array.Basic
{β : Type v} {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) : m β
Array.size_eq_length_toList 📋 Init.Data.Array.Basic
{α : Type u} {xs : Array α} : xs.size = xs.toList.length
Array.uget 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : USize) (h : i.toNat < xs.size) : α
Array.ugetBorrowed 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : USize) (h : i.toNat < xs.size) : α
Array.mapM 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β)
Array.mapMUnsafe 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β)
Array.modifyM 📋 Init.Data.Array.Basic
{α : Type u} {m : Type u → Type u_1} [Monad m] (xs : Array α) (i : ℕ) (f : α → m α) : m (Array α)
Array.modifyMUnsafe 📋 Init.Data.Array.Basic
{α : Type u} {m : Type u → Type u_1} [Monad m] (xs : Array α) (i : ℕ) (f : α → m α) : m (Array α)
Array.zipIdx 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (start : ℕ := 0) : Array (α × ℕ)
Array.zipWithAll 📋 Init.Data.Array.Basic
{α : Type u} {β : Type u_1} {γ : Type u_2} (f : Option α → Option β → γ) (as : Array α) (bs : Array β) : Array γ
Array.eraseIdx 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : ℕ) (h : i < xs.size := by get_elem_tactic) : Array α
Array.findSomeM? 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β)
Array.findSomeRevM? 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β)
Array.flatMapM 📋 Init.Data.Array.Basic
{α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β)
Array.mapIdxM 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : ℕ → α → m β) (as : Array α) : m (Array β)
Array.uset 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : USize) (v : α) (h : i.toNat < xs.size) : Array α
Array.insertIdx 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (i : ℕ) (a : α) : autoParam (i ≤ as.size) Array.insertIdx._auto_1 → Array α
Array.mapFinIdx 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} (as : Array α) (f : (i : ℕ) → α → i < as.size → β) : Array β
Array.back 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (h : 0 < xs.size := by get_elem_tactic) : α
Array.instForIn'InferInstanceMembershipOfMonad 📋 Init.Data.Array.Basic
{α : Type u} {m : Type u_1 → Type u_2} [Monad m] : ForIn' m (Array α) α inferInstance
Array.instGetElemUSizeLtNatToNatSize 📋 Init.Data.Array.Basic
{α : Type u} : GetElem (Array α) USize α fun xs i => i.toNat < xs.size
Array.popWhile_empty 📋 Init.Data.Array.Basic
{α : Type u} {p : α → Bool} : Array.popWhile p #[] = #[]
Array.all 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (p : α → Bool) (start : ℕ := 0) (stop : ℕ := as.size) : Bool
Array.any 📋 Init.Data.Array.Basic
{α : Type u} (as : Array α) (p : α → Bool) (start : ℕ := 0) (stop : ℕ := as.size) : Bool
Array.drop_eq_extract 📋 Init.Data.Array.Basic
{α : Type u} {xs : Array α} {i : ℕ} : xs.drop i = xs.extract i
Array.isPrefixOfAux 📋 Init.Data.Array.Basic
{α : Type u} [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : ℕ) : Bool
Array.swapAt 📋 Init.Data.Array.Basic
{α : Type u} (xs : Array α) (i : ℕ) (v : α) (hi : i < xs.size := by get_elem_tactic) : α × Array α
Array.zipWithM 📋 Init.Data.Array.Basic
{α : Type u} {β : Type u_1} {γ : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m γ) (as : Array α) (bs : Array β) : m (Array γ)
Array.Mem.mk 📋 Init.Data.Array.Basic
{α : Type u} {as : Array α} {a : α} (val : a ∈ as.toList) : as.Mem a
Array.Mem.val 📋 Init.Data.Array.Basic
{α : Type u} {as : Array α} {a : α} (self : as.Mem a) : a ∈ as.toList
Array.ext' 📋 Init.Data.Array.Basic
{α : Type u} {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys
Array.filter 📋 Init.Data.Array.Basic
{α : Type u} (p : α → Bool) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : Array α
Array.take_eq_extract 📋 Init.Data.Array.Basic
{α : Type u} {xs : Array α} {i : ℕ} : xs.take i = xs.extract 0 i
Array.filterMap 📋 Init.Data.Array.Basic
{α : Type u} {β : Type u_1} (f : α → Option β) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : Array β
Array.foldl 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : β
Array.foldr 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start : ℕ := as.size) (stop : ℕ := 0) : β
Array.zipWithMAux 📋 Init.Data.Array.Basic
{α : Type u} {β : Type u_1} {γ : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (bs : Array β) (f : α → β → m γ) (i : ℕ) (cs : Array γ) : m (Array γ)
Array.anyM.loop 📋 Init.Data.Array.Basic
{α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (stop : ℕ) (h : stop ≤ as.size) (j : ℕ) : m Bool
Array.mapFinIdxM 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (i : ℕ) → α → i < as.size → m β) : m (Array β)
Array.mem_def 📋 Init.Data.Array.Basic
{α : Type u} {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList
Array.mem_toArray 📋 Init.Data.Array.Basic
{α : Type u} {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l
List.mem_toArray 📋 Init.Data.Array.Basic
{α : Type u} {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l
Array.allM 📋 Init.Data.Array.Basic
{α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : m Bool
Array.anyM 📋 Init.Data.Array.Basic
{α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : m Bool
Array.anyMUnsafe 📋 Init.Data.Array.Basic
{α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : m Bool
Array.forIn' 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β
Array.forIn'Unsafe 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β
Array.forM 📋 Init.Data.Array.Basic
{α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit.{v + 1}) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : m PUnit.{v + 1}
Array.forRevM 📋 Init.Data.Array.Basic
{α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit.{v + 1}) (as : Array α) (start : ℕ := as.size) (stop : ℕ := 0) : m PUnit.{v + 1}
Array.foldrM.fold 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (as : Array α) (stop i : ℕ) (h : i ≤ as.size) (b : β) : m β
Array.filterM 📋 Init.Data.Array.Basic
{m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : m (Array α)
Array.filterRevM 📋 Init.Data.Array.Basic
{m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start : ℕ := as.size) (stop : ℕ := 0) : m (Array α)
Array.isEqvAux 📋 Init.Data.Array.Basic
{α : Type u} (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Bool) (i : ℕ) : i ≤ xs.size → Bool
Array.size_pop 📋 Init.Data.Array.Basic
{α : Type u} {xs : Array α} : xs.pop.size = xs.size - 1
Array.size_set 📋 Init.Data.Array.Basic
{α : Type u} {xs : Array α} {i : ℕ} {v : α} (h : i < xs.size) : (xs.set i v h).size = xs.size
Array.foldlM.loop 📋 Init.Data.Array.Basic
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (as : Array α) (stop : ℕ) (h : stop ≤ as.size) (i j : ℕ) (b : β) : m β
Array.filterMapM 📋 Init.Data.Array.Basic
{α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : α → m (Option β)) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : m (Array β)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 3a988db serving mathlib revision 8a897a4