Loogle!

Result

Found 47 declarations mentioning List.getD.

• List.getD 📋 Init.Data.List.BasicAux
  {α : Type u_1} (as : List α) (i : ℕ) (fallback : α) : α
• List.getD_nil 📋 Init.Data.List.BasicAux
  {n : ℕ} {α✝ : Type u_1} {d : α✝} : [].getD n d = d
• List.getD_cons_zero 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {x : α✝} {xs : List α✝} {d : α✝} : (x :: xs).getD 0 d = x
• List.getD_cons_succ 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {x : α✝} {xs : List α✝} {n : ℕ} {d : α✝} : (x :: xs).getD (n + 1) d = xs.getD n d
• List.getD_eq_getElem?_getD 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {i : ℕ} {a : α} : l.getD i a = l[i]?.getD a
• List.getD.eq_1 📋 Init.Data.List.Lemmas
  {α : Type u_1} (as : List α) (i : ℕ) (fallback : α) : as.getD i fallback = as[i]?.getD fallback
• BitVec.getLsbD_ofBoolListLE 📋 Init.Data.BitVec.Lemmas
  {bs : List Bool} {i : ℕ} : (BitVec.ofBoolListLE bs).getLsbD i = bs.getD i false
• BitVec.getLsb_ofBoolListLE 📋 Init.Data.BitVec.Lemmas
  {bs : List Bool} {i : ℕ} : (BitVec.ofBoolListLE bs).getLsbD i = bs.getD i false
• BitVec.getMsbD_ofBoolListBE 📋 Init.Data.BitVec.Lemmas
  {bs : List Bool} {i : ℕ} : (BitVec.ofBoolListBE bs).getMsbD i = bs.getD i false
• BitVec.getLsbD_ofBoolListBE 📋 Init.Data.BitVec.Lemmas
  {bs : List Bool} {i : ℕ} : (BitVec.ofBoolListBE bs).getLsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)
• BitVec.getMsbD_ofBoolListLE 📋 Init.Data.BitVec.Lemmas
  {bs : List Bool} {i : ℕ} : (BitVec.ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)
• Std.DTreeMap.Internal.Impl.entryAtIdxD_eq_getD 📋 Std.Data.DTreeMap.Internal.WF.Lemmas
  {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced) {i : ℕ} {fallback : (a : α) × β a} : t.entryAtIdxD i fallback = t.toListModel.getD i fallback
• List.decidableGetDNilNe 📋 Mathlib.Data.List.GetD
  {α : Type u} (a : α) : DecidablePred fun i => [].getD i a ≠ a
• List.getD_default_eq_getI 📋 Mathlib.Data.List.GetD
  {α : Type u} (l : List α) [Inhabited α] {n : ℕ} : l.getD n default = l.getI n
• List.getD_eq_default 📋 Mathlib.Data.List.GetD
  {α : Type u} (l : List α) (d : α) {n : ℕ} (hn : l.length ≤ n) : l.getD n d = d
• List.getD_replicate 📋 Mathlib.Data.List.GetD
  {α : Type u} (x : α) {y : α} {i n : ℕ} (h : i < n) : (List.replicate n x).getD i y = x
• List.getD_map 📋 Mathlib.Data.List.GetD
  {α : Type u} {β : Type v} (l : List α) (d : α) {n : ℕ} (f : α → β) : (List.map f l).getD n (f d) = f (l.getD n d)
• List.getD_eq_getD_getElem? 📋 Mathlib.Data.List.GetD
  {α : Type u} (l : List α) (d : α) (n : ℕ) : l.getD n d = l[n]?.getD d
• List.getD_append 📋 Mathlib.Data.List.GetD
  {α : Type u} (l l' : List α) (d : α) (n : ℕ) (h : n < l.length) : (l ++ l').getD n d = l.getD n d
• List.getD_eq_getElem 📋 Mathlib.Data.List.GetD
  {α : Type u} (l : List α) (d : α) {n : ℕ} (hn : n < l.length) : l.getD n d = l[n]
• List.getD_reverse 📋 Mathlib.Data.List.GetD
  {α : Type u} {l : List α} (i : ℕ) (h : i < l.length) : l.reverse.getD i = l.getD (l.length - 1 - i)
• List.getD_append_right 📋 Mathlib.Data.List.GetD
  {α : Type u} (l l' : List α) (d : α) (n : ℕ) (h : l.length ≤ n) : (l ++ l').getD n d = l'.getD (n - l.length) d
• List.toFinsupp 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => l.getD x 0 ≠ 0] : ℕ →₀ M
• List.toFinsupp_nil 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] [DecidablePred fun i => [].getD i 0 ≠ 0] : [].toFinsupp = 0
• List.toFinsupp_singleton 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] (x : M) [DecidablePred fun x_1 => [x].getD x_1 0 ≠ 0] : [x].toFinsupp = fun₀ | 0 => x
• List.coe_toFinsupp 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => l.getD x 0 ≠ 0] : ⇑l.toFinsupp = fun x => l.getD x 0
• List.toFinsupp_apply 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => l.getD x 0 ≠ 0] (i : ℕ) : l.toFinsupp i = l.getD i 0
• List.toFinsupp_apply_le 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => l.getD x 0 ≠ 0] (n : ℕ) (hn : l.length ≤ n) : l.toFinsupp n = 0
• List.toFinsupp_support 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => l.getD x 0 ≠ 0] : l.toFinsupp.support = {i ∈ Finset.range l.length | l.getD i 0 ≠ 0}
• List.toFinsupp.congr_simp 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] (l l✝ : List M) (e_l : l = l✝) {inst✝ : DecidablePred fun x => l.getD x 0 ≠ 0} [DecidablePred fun x => l✝.getD x 0 ≠ 0] : l.toFinsupp = l✝.toFinsupp
• List.toFinsupp_apply_lt 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => l.getD x 0 ≠ 0] (n : ℕ) (hn : n < l.length) : l.toFinsupp n = l[n]
• List.toFinsupp_eq_sum_mapIdx_single 📋 Mathlib.Data.List.ToFinsupp
  {R : Type u_2} [AddMonoid R] (l : List R) [DecidablePred fun x => l.getD x 0 ≠ 0] : l.toFinsupp = (List.mapIdx (fun n r => fun₀ | n => r) l).sum
• List.toFinsupp_apply_fin 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => l.getD x 0 ≠ 0] (n : Fin l.length) : l.toFinsupp ↑n = l[n]
• List.toFinsupp_cons_eq_single_add_embDomain 📋 Mathlib.Data.List.ToFinsupp
  {R : Type u_2} [AddZeroClass R] (x : R) (xs : List R) [DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0] [DecidablePred fun x => xs.getD x 0 ≠ 0] : (x :: xs).toFinsupp = (fun₀ | 0 => x) + Finsupp.embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } xs.toFinsupp
• List.toFinsupp_concat_eq_toFinsupp_add_single 📋 Mathlib.Data.List.ToFinsupp
  {R : Type u_2} [AddZeroClass R] (x : R) (xs : List R) [DecidablePred fun i => (xs ++ [x]).getD i 0 ≠ 0] [DecidablePred fun i => xs.getD i 0 ≠ 0] : (xs ++ [x]).toFinsupp = xs.toFinsupp + fun₀ | xs.length => x
• List.toFinsupp_append 📋 Mathlib.Data.List.ToFinsupp
  {R : Type u_2} [AddZeroClass R] (l₁ l₂ : List R) [DecidablePred fun x => (l₁ ++ l₂).getD x 0 ≠ 0] [DecidablePred fun x => l₁.getD x 0 ≠ 0] [DecidablePred fun x => l₂.getD x 0 ≠ 0] : (l₁ ++ l₂).toFinsupp = l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp
• Polynomial.ofFn.eq_1 📋 Mathlib.Algebra.Polynomial.OfFn
  {R : Type u_1} [Semiring R] [DecidableEq R] (n : ℕ) : Polynomial.ofFn n = { toFun := fun v => { toFinsupp := (List.ofFn v).toFinsupp }, map_add' := ⋯, map_smul' := ⋯ }
• SimpleGraph.Walk.getVert_eq_getD_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : p.getVert n = p.support.getD n v
• Primrec.list_getD 📋 Mathlib.Computability.Primrec
  {α : Type u_1} [Primcodable α] (d : α) : Primrec₂ fun l n => l.getD n d
• Nat.nth_eq_getD_sort 📋 Mathlib.Data.Nat.Nth
  {p : ℕ → Prop} (h : (setOf p).Finite) (n : ℕ) : Nat.nth p n = (h.toFinset.sort fun a b => a ≤ b).getD n 0
• Nat.nth.eq_1 📋 Mathlib.Data.Nat.Nth
  (p : ℕ → Prop) (n : ℕ) : Nat.nth p n = if h : (setOf p).Finite then (h.toFinset.sort fun a b => a ≤ b).getD n 0 else ↑((Nat.Subtype.orderIsoOfNat (setOf p)) n)
• CoxeterSystem.getD_leftInvSeq_mul_wordProd 📋 Mathlib.GroupTheory.Coxeter.Inversion
  {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : (cs.leftInvSeq ω).getD j 1 * cs.wordProd ω = cs.wordProd (ω.eraseIdx j)
• CoxeterSystem.wordProd_mul_getD_rightInvSeq 📋 Mathlib.GroupTheory.Coxeter.Inversion
  {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : cs.wordProd ω * (cs.rightInvSeq ω).getD j 1 = cs.wordProd (ω.eraseIdx j)
• CoxeterSystem.getD_leftInvSeq_mul_self 📋 Mathlib.GroupTheory.Coxeter.Inversion
  {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : (cs.leftInvSeq ω).getD j 1 * (cs.leftInvSeq ω).getD j 1 = 1
• CoxeterSystem.getD_rightInvSeq_mul_self 📋 Mathlib.GroupTheory.Coxeter.Inversion
  {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : (cs.rightInvSeq ω).getD j 1 * (cs.rightInvSeq ω).getD j 1 = 1
• CoxeterSystem.getD_leftInvSeq 📋 Mathlib.GroupTheory.Coxeter.Inversion
  {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : (cs.leftInvSeq ω).getD j 1 = cs.wordProd (List.take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (List.take j ω))⁻¹
• CoxeterSystem.getD_rightInvSeq 📋 Mathlib.GroupTheory.Coxeter.Inversion
  {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : (cs.rightInvSeq ω).getD j 1 = (cs.wordProd (List.drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (List.drop (j + 1) ω)

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 187ba29 serving mathlib revision 6c19380