Loogle!

Result

Found 23 declarations whose name contains "append_singleton".

• List.append_singleton_inj 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a b : α} {as bs : List α} : as ++ [a] = bs ++ [b] ↔ as = bs ∧ a = b
• Array.append_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {a : α} {as : Array α} : as ++ #[a] = as.push a
• Array.push_eq_append_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {as : Array α} {x : α} : as.push x = as ++ #[x]
• Array.append_singleton_assoc 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {a : α} {xs ys : Array α} : xs ++ (#[a] ++ ys) = xs.push a ++ ys
• String.append_singleton 📋 Init.Data.String.Defs
  {s : String} {c : Char} : s ++ String.singleton c = s.push c
• String.Pos.Splits.exists_eq_append_singleton 📋 Init.Data.String.Lemmas.Splits
  {t₁ t₂ s : String} {p : s.Pos} (hp : p ≠ s.endPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ String.singleton (p.get hp)
• String.Slice.Pos.Splits.exists_eq_append_singleton 📋 Init.Data.String.Lemmas.Splits
  {t₁ t₂ : String} {s : String.Slice} {p : s.Pos} (hp : p ≠ s.endPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ String.singleton (p.get hp)
• String.Pos.Splits.exists_eq_append_singleton_of_ne_startPos 📋 Init.Data.String.Lemmas.Splits
  {t₁ t₂ s : String} {p : s.Pos} (hp : p ≠ s.startPos) (h : p.Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ String.singleton ((p.prev hp).get ⋯)
• String.Slice.Pos.Splits.exists_eq_append_singleton_of_ne_startPos 📋 Init.Data.String.Lemmas.Splits
  {t₁ t₂ : String} {s : String.Slice} {p : s.Pos} (hp : p ≠ s.startPos) (h : p.Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ String.singleton ((p.prev hp).get ⋯)
• Vector.append_singleton 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n} : xs ++ #v[a] = xs.push a
• List.perm_append_singleton 📋 Init.Data.List.Perm
  {α : Type u_1} (a : α) (l : List α) : (l ++ [a]).Perm (a :: l)
• List.getLast_append_singleton 📋 Mathlib.Data.List.Basic
  {α : Type u} {a : α} (l : List α) : (l ++ [a]).getLast ⋯ = a
• List.tail_append_singleton_of_ne_nil 📋 Mathlib.Data.List.Basic
  {α : Type u} {a : α} {l : List α} (h : l ≠ []) : (l ++ [a]).tail = l.tail ++ [a]
• List.chain_append_singleton_iff_forall₂ 📋 Mathlib.Data.List.Chain
  {α : Type u} {R : α → α → Prop} {l : List α} {a b : α} : List.IsChain R (a :: l ++ [b]) ↔ List.Forall₂ R (a :: l) (l ++ [b])
• List.isChain_cons_append_singleton_iff_forall₂ 📋 Mathlib.Data.List.Chain
  {α : Type u} {R : α → α → Prop} {l : List α} {a b : α} : List.IsChain R (a :: l ++ [b]) ↔ List.Forall₂ R (a :: l) (l ++ [b])
• List.IsRotated.cons_append_singleton 📋 Mathlib.Data.List.Rotate
  {α : Type u} {l : List α} {a : α} : a :: l ~r l ++ [a]
• RelSeries.append_singleton_left 📋 Mathlib.Order.RelSeries
  {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (x : α) (hx : (x, p.head) ∈ r) : (RelSeries.singleton r x).append p hx = p.cons x hx
• DFA.eval_append_singleton 📋 Mathlib.Computability.DFA
  {α : Type u} {σ : Type v} (M : DFA α σ) (x : List α) (a : α) : M.eval (x ++ [a]) = M.step (M.eval x) a
• DFA.evalFrom_append_singleton 📋 Mathlib.Computability.DFA
  {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (x : List α) (a : α) : M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a
• NFA.eval_append_singleton 📋 Mathlib.Computability.NFA
  {α : Type u} {σ : Type v} (M : NFA α σ) (x : List α) (a : α) : M.eval (x ++ [a]) = M.stepSet (M.eval x) a
• NFA.evalFrom_append_singleton 📋 Mathlib.Computability.NFA
  {α : Type u} {σ : Type v} {M : NFA α σ} (S : Set σ) (x : List α) (a : α) : M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a
• εNFA.eval_append_singleton 📋 Mathlib.Computability.EpsilonNFA
  {α : Type u} {σ : Type v} (M : εNFA α σ) (x : List α) (a : α) : M.eval (x ++ [a]) = M.stepSet (M.eval x) a
• εNFA.evalFrom_append_singleton 📋 Mathlib.Computability.EpsilonNFA
  {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) (x : List α) (a : α) : M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a

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.

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

This is Loogle revision 128218b serving mathlib revision 6682a4e