Loogle!

Result

Found 18 declarations mentioning Turing.ListBlank.map.

• Turing.ListBlank.map 📋 Mathlib.Computability.Tape
  {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (l : Turing.ListBlank Γ) : Turing.ListBlank Γ'
• Turing.ListBlank.head_map 📋 Mathlib.Computability.Tape
  {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (l : Turing.ListBlank Γ) : (Turing.ListBlank.map f l).head = f.f l.head
• Turing.ListBlank.tail_map 📋 Mathlib.Computability.Tape
  {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (l : Turing.ListBlank Γ) : (Turing.ListBlank.map f l).tail = Turing.ListBlank.map f l.tail
• Turing.ListBlank.nth_map 📋 Mathlib.Computability.Tape
  {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (l : Turing.ListBlank Γ) (n : ℕ) : (Turing.ListBlank.map f l).nth n = f.f (l.nth n)
• Turing.ListBlank.map_mk 📋 Mathlib.Computability.Tape
  {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (l : List Γ) : Turing.ListBlank.map f (Turing.ListBlank.mk l) = Turing.ListBlank.mk (List.map f.f l)
• Turing.ListBlank.map_cons 📋 Mathlib.Computability.Tape
  {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (l : Turing.ListBlank Γ) (a : Γ) : Turing.ListBlank.map f (Turing.ListBlank.cons a l) = Turing.ListBlank.cons (f.f a) (Turing.ListBlank.map f l)
• Turing.Tape.map_mk' 📋 Mathlib.Computability.Tape
  {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (L R : Turing.ListBlank Γ) : Turing.Tape.map f (Turing.Tape.mk' L R) = Turing.Tape.mk' (Turing.ListBlank.map f L) (Turing.ListBlank.map f R)
• Turing.proj_map_nth 📋 Mathlib.Computability.Tape
  {ι : Type u_1} {Γ : ι → Type u_2} [(i : ι) → Inhabited (Γ i)] (i : ι) (L : Turing.ListBlank ((i : ι) → Γ i)) (n : ℕ) : (Turing.ListBlank.map (Turing.proj i) L).nth n = L.nth n i
• Turing.Tape.map.eq_1 📋 Mathlib.Computability.Tape
  {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (T : Turing.Tape Γ) : Turing.Tape.map f T = { head := f.f T.head, left := Turing.ListBlank.map f T.left, right := Turing.ListBlank.map f T.right }
• Turing.ListBlank.map_modifyNth 📋 Mathlib.Computability.Tape
  {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (F : Turing.PointedMap Γ Γ') (f : Γ → Γ) (f' : Γ' → Γ') (H : ∀ (x : Γ), F.f (f x) = f' (F.f x)) (n : ℕ) (L : Turing.ListBlank Γ) : Turing.ListBlank.map F (Turing.ListBlank.modifyNth f n L) = Turing.ListBlank.modifyNth f' n (Turing.ListBlank.map F L)
• Turing.TM2to1.addBottom_map 📋 Mathlib.Computability.TuringMachine
  {K : Type u_1} {Γ : K → Type u_2} (L : Turing.ListBlank ((k : K) → Option (Γ k))) : Turing.ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (Turing.TM2to1.addBottom L) = L
• Turing.TM2to1.addBottom.eq_1 📋 Mathlib.Computability.TuringMachine
  {K : Type u_1} {Γ : K → Type u_2} (L : Turing.ListBlank ((k : K) → Option (Γ k))) : Turing.TM2to1.addBottom L = Turing.ListBlank.cons (true, L.head) (Turing.ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)
• Turing.TM2to1.stk_nth_val 📋 Mathlib.Computability.TuringMachine
  {K : Type u_1} {Γ : K → Type u_2} {L : Turing.ListBlank ((k : K) → Option (Γ k))} {k : K} {S : List (Γ k)} (n : ℕ) (hL : Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some S).reverse) : L.nth n k = S.reverse[n]?
• Turing.TM2to1.TrCfg.mk 📋 Mathlib.Computability.TuringMachine
  {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {q : Option Λ} {v : σ} {S : (k : K) → List (Γ k)} (L : Turing.ListBlank ((k : K) → Option (Γ k))) : (∀ (k : K), Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some (S k)).reverse) → Turing.TM2to1.TrCfg { l := q, var := v, stk := S } { l := Option.map Turing.TM2to1.Λ'.normal q, var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) }
• Turing.TM2to1.tr_eval 📋 Mathlib.Computability.TuringMachine
  {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) [Inhabited Λ] [Inhabited σ] (k : K) (L : List (Γ k)) {L₁ : Turing.ListBlank (Turing.TM2to1.Γ' K Γ)} {L₂ : List (Γ k)} (H₁ : L₁ ∈ Turing.TM1.eval (Turing.TM2to1.tr M) (Turing.TM2to1.trInit k L)) (H₂ : L₂ ∈ Turing.TM2.eval M k L) : ∃ S L', Turing.TM2to1.addBottom L' = L₁ ∧ (∀ (k : K), Turing.ListBlank.map (Turing.proj k) L' = Turing.ListBlank.mk (List.map some (S k)).reverse) ∧ S k = L₂
• Turing.TM2to1.tr_respects_aux₁ 📋 Mathlib.Computability.TuringMachine
  {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) {k : K} (o : Turing.TM2to1.StAct K Γ σ k) (q : Turing.TM2.Stmt Γ Λ σ) (v : σ) {S : List (Γ k)} {L : Turing.ListBlank ((k : K) → Option (Γ k))} (hL : Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some S).reverse) (n : ℕ) (H : n ≤ S.length) : Turing.Reaches₀ (Turing.TM1.step (Turing.TM2to1.tr M)) { l := some (Turing.TM2to1.Λ'.go k o q), var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) } { l := some (Turing.TM2to1.Λ'.go k o q), var := v, Tape := (Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L)) }
• Turing.TM2to1.tr_respects_aux₂ 📋 Mathlib.Computability.TuringMachine
  {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] {k : K} {q : Turing.TM1.Stmt (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ} {v : σ} {S : (k : K) → List (Γ k)} {L : Turing.ListBlank ((k : K) → Option (Γ k))} (hL : ∀ (k : K), Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some (S k)).reverse) (o : Turing.TM2to1.StAct K Γ σ k) : let v' := Turing.TM2to1.stVar v (S k) o; let Sk' := Turing.TM2to1.stWrite v (S k) o; let S' := Function.update S k Sk'; ∃ L', (∀ (k : K), Turing.ListBlank.map (Turing.proj k) L' = Turing.ListBlank.mk (List.map some (S' k)).reverse) ∧ Turing.TM1.stepAux (Turing.TM2to1.trStAct q o) v ((Turing.Tape.move Turing.Dir.right)^[(S k).length] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L))) = Turing.TM1.stepAux q v' ((Turing.Tape.move Turing.Dir.right)^[(S' k).length] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L')))
• Turing.TM2to1.tr_respects_aux 📋 Mathlib.Computability.TuringMachine
  {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) {q : Turing.TM2.Stmt Γ Λ σ} {v : σ} {T : Turing.ListBlank ((i : K) → Option (Γ i))} {k : K} {S : (k : K) → List (Γ k)} (hT : ∀ (k : K), Turing.ListBlank.map (Turing.proj k) T = Turing.ListBlank.mk (List.map some (S k)).reverse) (o : Turing.TM2to1.StAct K Γ σ k) (IH : ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : Turing.ListBlank ((k : K) → Option (Γ k))}, (∀ (k : K), Turing.ListBlank.map (Turing.proj k) T = Turing.ListBlank.mk (List.map some (S k)).reverse) → ∃ b, Turing.TM2to1.TrCfg (Turing.TM2.stepAux q v S) b ∧ Turing.Reaches (Turing.TM1.step (Turing.TM2to1.tr M)) (Turing.TM1.stepAux (Turing.TM2to1.trNormal q) v (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom T))) b) : ∃ b, Turing.TM2to1.TrCfg (Turing.TM2.stepAux (Turing.TM2to1.stRun o q) v S) b ∧ Turing.Reaches (Turing.TM1.step (Turing.TM2to1.tr M)) (Turing.TM1.stepAux (Turing.TM2to1.trNormal (Turing.TM2to1.stRun o q)) v (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom T))) b

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 40fea08