Loogle!

Result

Found 7257 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 α
• 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
• Lean.Syntax.getHeadInfo?.loop 📋 Init.Prelude
  (args : Array Lean.Syntax) (i : ℕ) : Option Lean.SourceInfo
• 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.get!Internal 📋 Init.Prelude
  {α : Type u} [Inhabited α] (a : Array α) (i : ℕ) : α
• Array.mkArray5 📋 Init.Prelude
  {α : Type u} (a₁ a₂ a₃ a₄ a₅ : α) : Array α
• Lean.Syntax.getTailPos?.loop 📋 Init.Prelude
  (canonicalOnly : Bool := false) (args : Array Lean.Syntax) (i : ℕ) : Option String.Pos
• 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.extract 📋 Init.Prelude
  {α : Type u_1} (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : Array α
• Lean.Syntax.SepArray.mk.sizeOf_spec 📋 Init.SizeOf
  {sep : String} (elemsAndSeps : Array Lean.Syntax) : sizeOf { elemsAndSeps := elemsAndSeps } = 1 + sizeOf elemsAndSeps
• Array.mk.sizeOf_spec 📋 Init.SizeOf
  {α : Type u} [SizeOf α] (toList : List α) : sizeOf { toList := toList } = 1 + sizeOf toList
• Lean.Syntax.TSepArray.mk.sizeOf_spec 📋 Init.SizeOf
  {ks : Lean.SyntaxNodeKinds} {sep : String} (elemsAndSeps : Array Lean.Syntax) : sizeOf { elemsAndSeps := elemsAndSeps } = 1 + sizeOf elemsAndSeps
• Lean.Syntax.node.sizeOf_spec 📋 Init.SizeOf
  (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax) : sizeOf (Lean.Syntax.node info kind args) = 1 + sizeOf info + sizeOf kind + sizeOf args
• Array.mk.injEq 📋 Init.Core
  {α : Type u} (toList toList✝ : List α) : ({ toList := toList } = { toList := toList✝ }) = (toList = toList✝)
• Lean.Syntax.node.injEq 📋 Init.Core
  (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax) (info✝ : Lean.SourceInfo) (kind✝ : Lean.SyntaxNodeKind) (args✝ : Array Lean.Syntax) : (Lean.Syntax.node info kind args = Lean.Syntax.node info✝ kind✝ args✝) = (info = info✝ ∧ kind = kind✝ ∧ args = args✝)
• 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
• Lean.Module.mk.injEq 📋 Init.MetaTypes
  (header : Lean.Syntax) (commands : Array Lean.Syntax) (header✝ : Lean.Syntax) (commands✝ : Array Lean.Syntax) : ({ header := header, commands := commands } = { header := header✝, commands := commands✝ }) = (header = header✝ ∧ commands = commands✝)
• Lean.Module.mk.sizeOf_spec 📋 Init.MetaTypes
  (header : Lean.Syntax) (commands : Array Lean.Syntax) : sizeOf { header := header, commands := commands } = 1 + sizeOf header + sizeOf commands
• Option.toArray 📋 Init.Data.Option.Basic
  {α : Type u_1} : Option α → Array α
• 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_1 📋 Init.GetElem
  {α : Type u} [Inhabited α] (a : Array α) (i : ℕ) : a.get!Internal i = a.getD i default
• 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.setD 📋 Init.Data.Array.Set
  {α : Type u_1} (xs : Array α) (i : ℕ) (v : α) : 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} (a : 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.data 📋 Init.Data.Array.Basic
  {α : Type u_1} (self : Array α) : List α
• Array.getEvenElems 📋 Init.Data.Array.Basic
  {α : Type u} (as : Array α) : Array α
• Array.instMembership 📋 Init.Data.Array.Basic
  {α : Type u} : Membership α (Array α)
• Array.mkArray 📋 Init.Data.Array.Basic
  {α : Type u} (n : ℕ) (v : α) : 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.get? 📋 Init.Data.Array.Basic
  {α : Type u} (xs : Array α) (i : ℕ) : Option α
• 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.instToString 📋 Init.Data.Array.Basic
  {α : Type u} [ToString α] : ToString (Array α)
• Array.reduceOption 📋 Init.Data.Array.Basic
  {α : Type u} (as : Array (Option α)) : Array α
• 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.Array.repr 📋 Init.Data.Array.Basic
  {α : Type u} [Repr α] (xs : Array α) : Std.Format
• Array.shrink.loop 📋 Init.Data.Array.Basic
  {α : Type u} : ℕ → Array α → 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.insertAt! 📋 Init.Data.Array.Basic
  {α : Type u_1} (as : Array α) (i : ℕ) (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.getIdx? 📋 Init.Data.Array.Basic
  {α : Type u} [BEq α] (xs : Array α) (v : α) : Option ℕ
• 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.instForM 📋 Init.Data.Array.Basic
  {α : Type u} {m : Type u_1 → Type u_2} : ForM m (Array α) α
• 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.swap! 📋 Init.Data.Array.Basic
  {α : Type u_1} (xs : Array α) (i j : ℕ) : 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.concatMap 📋 Init.Data.Array.Basic
  {α : Type u_1} {β : Type u_2} (f : α → Array β) (as : Array α) : Array β
• 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.partition 📋 Init.Data.Array.Basic
  {α : Type u} (p : α → Bool) (as : Array α) : Array α × Array α
• Array.split 📋 Init.Data.Array.Basic
  {α : Type u} (as : Array α) (p : α → Bool) : Array α × Array α
• Array.zip 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type u_1} (as : Array α) (bs : Array β) : Array (α × β)
• Array.insertIdx.loop 📋 Init.Data.Array.Basic
  {α : Type u} (i : ℕ) (as : Array α) (j : Fin as.size) : Array α
• Array.ofFn.go 📋 Init.Data.Array.Basic
  {α : Type u} {n : ℕ} (f : Fin n → α) (i : ℕ) (acc : Array α) : Array α
• Array.reverse.loop 📋 Init.Data.Array.Basic
  {α : Type u} (as : Array α) (i : ℕ) (j : Fin as.size) : Array α
• Array.takeWhile.go 📋 Init.Data.Array.Basic
  {α : Type u} (p : α → Bool) (as : Array α) (i : ℕ) (acc : Array α) : Array α
• Array.finIdxOf? 📋 Init.Data.Array.Basic
  {α : Type u} [BEq α] (xs : Array α) (v : α) : Option (Fin xs.size)
• Array.indexOf? 📋 Init.Data.Array.Basic
  {α : Type u_1} [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.findFinIdx?.loop 📋 Init.Data.Array.Basic
  {α : Type u} (p : α → Bool) (as : Array α) (j : ℕ) : Option (Fin as.size)
• Array.idxOfAux 📋 Init.Data.Array.Basic
  {α : Type u} [BEq α] (xs : Array α) (v : α) (i : ℕ) : Option (Fin xs.size)
• Array.indexOfAux 📋 Init.Data.Array.Basic
  {α : Type u_1} [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 γ
• List.toArray_toList 📋 Init.Data.Array.Basic
  {α : Type u_1} {xs : Array α} : xs.toList.toArray = xs
• Array.usize.eq_1 📋 Init.Data.Array.Basic
  {α : Type u} (a : Array α) : a.usize = a.size.toUSize
• List.toArrayAux.eq_1 📋 Init.Data.Array.Basic
  {α : Type u_1} (x✝ : Array α) : [].toArrayAux x✝ = x✝
• 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} (a : Array α) (i : USize) (h : i.toNat < a.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.sequenceMap 📋 Init.Data.Array.Basic
  {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] (f : α → m β) (as : Array α) : 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.zipWithIndex 📋 Init.Data.Array.Basic
  {α : Type u_1} (xs : Array α) (start : ℕ := 0) : Array (α × ℕ)
• Array.anyMUnsafe.any 📋 Init.Data.Array.Basic
  {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (i stop : USize) : m Bool
• Array.firstM.go 📋 Init.Data.Array.Basic
  {β : Type v} {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) (i : ℕ) : m β
• Array.concatMapM 📋 Init.Data.Array.Basic
  {α : Type u_1} {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (f : α → m (Array β)) (as : Array α) : m (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.instForIn'InferInstanceMembership 📋 Init.Data.Array.Basic
  {α : Type u} {m : Type u_1 → Type u_2} : ForIn' m (Array α) α inferInstance
• 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.zipWithAux 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type u_1} {γ : Type u_2} (as : Array α) (bs : Array β) (f : α → β → γ) (i : ℕ) (cs : Array γ) : Array γ
• Array.insertAt 📋 Init.Data.Array.Basic
  {α : Type u_1} (as : Array α) (i : ℕ) (a : α) : autoParam (i ≤ as.size) _auto✝ → Array α
• Array.insertIdx 📋 Init.Data.Array.Basic
  {α : Type u} (as : Array α) (i : ℕ) (a : α) : autoParam (i ≤ as.size) _auto✝ → Array α
• Array.mapFinIdx 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} (as : Array α) (f : (i : ℕ) → α → i < as.size → β) : Array β
• Array.mapMUnsafe.map 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (sz i : USize) (bs : Array NonScalar) : m (Array PNonScalar)
• Array.pop.eq_1 📋 Init.Data.Array.Basic
  {α : Type u} (xs : Array α) : xs.pop = { toList := xs.toList.dropLast }
• Array.back 📋 Init.Data.Array.Basic
  {α : Type u} (xs : Array α) (h : 0 < xs.size := by get_elem_tactic) : α
• 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.foldlMUnsafe.fold 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (as : Array α) (i stop : USize) (b : β) : m β
• Array.foldrMUnsafe.fold 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (as : Array α) (i stop : USize) (b : β) : m β
• Array.mapM.map 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) (i : ℕ) (bs : Array β) : m (Array β)
• Array.zipWithAll.go 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type u_1} {γ : Type u_2} (f : Option α → Option β → γ) (as : Array α) (bs : Array β) (i : ℕ) (cs : Array γ) : Array γ
• Array.all 📋 Init.Data.Array.Basic
  {α : Type u} (as : Array α) (p : α → Bool) (start : ℕ := 0) (stop : ℕ := as.size) : Bool

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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.

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.

This is Loogle revision 19971e9 serving mathlib revision 5f22769