Loogle!

Result

Found 237 declarations mentioning Computation. Of these, only the first 200 are shown.

• Computation 📋 Mathlib.Data.Seq.Computation
  (α : Type u) : Type u
• Computation.instAlternativeComputation 📋 Mathlib.Data.Seq.Computation
  : Alternative Computation
• Computation.instBind 📋 Mathlib.Data.Seq.Computation
  : Bind Computation
• Computation.monad 📋 Mathlib.Data.Seq.Computation
  : Monad Computation
• Computation.empty 📋 Mathlib.Data.Seq.Computation
  (α : Type u_1) : Computation α
• Computation.instLawfulMonad 📋 Mathlib.Data.Seq.Computation
  : LawfulMonad Computation
• Computation.Terminates 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) : Prop
• Computation.instInhabited 📋 Mathlib.Data.Seq.Computation
  {α : Type u} : Inhabited (Computation α)
• Computation.pure 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (a : α) : Computation α
• Computation.run 📋 Mathlib.Data.Seq.Computation
  {α : Type u} : Computation α → α
• Computation.Mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) (a : α) : Prop
• Computation.Promises 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) (a : α) : Prop
• Computation.head 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c : Computation α) : Option α
• Computation.instCoeTC 📋 Mathlib.Data.Seq.Computation
  {α : Type u} : CoeTC α (Computation α)
• Computation.instMembership 📋 Mathlib.Data.Seq.Computation
  {α : Type u} : Membership α (Computation α)
• Computation.tail 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c : Computation α) : Computation α
• Computation.think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c : Computation α) : Computation α
• Computation.Equiv 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c₁ c₂ : Computation α) : Prop
• Computation.Results 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) (a : α) (n : ℕ) : Prop
• Computation.join 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c : Computation (Computation α)) : Computation α
• Computation.runFor 📋 Mathlib.Data.Seq.Computation
  {α : Type u} : Computation α → ℕ → Option α
• Computation.thinkN 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c : Computation α) : ℕ → Computation α
• Computation.Equiv.equivalence 📋 Mathlib.Data.Seq.Computation
  {α : Type u} : Equivalence Computation.Equiv
• Computation.IsBisimulation 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (R : Computation α → Computation α → Prop) : Prop
• Computation.destruct 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c : Computation α) : α ⊕ Computation α
• Computation.get 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] : α
• Computation.length 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] : ℕ
• Computation.Equiv.refl 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) : s.Equiv s
• Computation.map 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : α → β) : Computation α → Computation β
• Computation.orElse 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c₁ : Computation α) (c₂ : Unit → Computation α) : Computation α
• Computation.bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (c : Computation α) (f : α → Computation β) : Computation β
• Computation.corec 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : β → α ⊕ β) (b : β) : Computation α
• Computation.think_equiv 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) : s.think.Equiv s
• Computation.LiftRel 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β) : Prop
• Computation.tail_empty 📋 Mathlib.Data.Seq.Computation
  {α : Type u} : (Computation.empty α).tail = Computation.empty α
• Computation.think_empty 📋 Mathlib.Data.Seq.Computation
  {α : Type u} : Computation.empty α = (Computation.empty α).think
• Computation.of_think_terminates 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} : s.think.Terminates → s.Terminates
• Computation.thinkN_equiv 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) (n : ℕ) : (s.thinkN n).Equiv s
• Computation.think_terminates 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [s.Terminates] : s.think.Terminates
• Computation.notMem_empty 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (a : α) : a ∉ Computation.empty α
• Computation.ret_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (a : α) : a ∈ Computation.pure a
• Computation.tail_think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) : s.think.tail = s
• Computation.bind_pure' 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) : s.bind Computation.pure = s
• Computation.eq_empty_of_not_terminates 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} (H : ¬s.Terminates) : s = Computation.empty α
• Computation.get_promises 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] : s.Promises s.get
• Computation.head_think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) : s.think.head = none
• Computation.map_id 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) : Computation.map id s = s
• Computation.of_thinkN_terminates 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) (n : ℕ) : (s.thinkN n).Terminates → s.Terminates
• Computation.tail_pure 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (a : α) : (Computation.pure a).tail = Computation.pure a
• Computation.thinkN_terminates 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [s.Terminates] (n : ℕ) : (s.thinkN n).Terminates
• Computation.Bind.g 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} : β ⊕ Computation β → β ⊕ Computation α ⊕ Computation β
• Computation.Equiv.symm 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s t : Computation α} : s.Equiv t → t.Equiv s
• Computation.Results.terminates 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} {n : ℕ} (h : s.Results a n) : s.Terminates
• Computation.LiftRel.equiv 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (R : α → α → Prop) (H : Equivalence R) : Equivalence (Computation.LiftRel R)
• Computation.LiftRel.refl 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (R : α → α → Prop) [Std.Refl R] : Std.Refl (Computation.LiftRel R)
• Computation.LiftRel.symm 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (R : α → α → Prop) [Std.Symm R] : Std.Symm (Computation.LiftRel R)
• Computation.LiftRel.trans 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (R : α → α → Prop) [IsTrans α R] : IsTrans (Computation α) (Computation.LiftRel R)
• Computation.BisimO 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (R : Computation α → Computation α → Prop) : α ⊕ Computation α → α ⊕ Computation α → Prop
• Computation.terminates_of_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} (h : a ∈ s) : s.Terminates
• Computation.destruct_empty 📋 Mathlib.Data.Seq.Computation
  {α : Type u} : (Computation.empty α).destruct = Sum.inr (Computation.empty α)
• Computation.mem_promises 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} : a ∈ s → s.Promises a
• Computation.terminates_congr 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {c₁ c₂ : Computation α} (h : c₁.Equiv c₂) : c₁.Terminates ↔ c₂.Terminates
• Computation.terminates_map 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : α → β) (s : Computation α) [s.Terminates] : (Computation.map f s).Terminates
• Computation.Mem.left_unique 📋 Mathlib.Data.Seq.Computation
  {α : Type u} : Relator.LeftUnique fun x1 x2 => x1 ∈ x2
• Computation.destruct_pure 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (a : α) : (Computation.pure a).destruct = Sum.inl a
• Computation.eq_of_pure_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {a a' : α} (h : a' ∈ Computation.pure a) : a' = a
• Computation.get_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] : s.get ∈ s
• Computation.pure_def 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (a : α) : pure a = Computation.pure a
• Computation.results_of_terminates 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [_T : s.Terminates] : s.Results s.get s.length
• Computation.terminates_map_iff 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : α → β) (s : Computation α) : (Computation.map f s).Terminates ↔ s.Terminates
• Computation.Bind.f 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : α → Computation β) : Computation α ⊕ Computation β → β ⊕ Computation α ⊕ Computation β
• Computation.Terminates.mk 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} (term : ∃ a, a ∈ s) : s.Terminates
• Computation.Terminates.term 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} [self : s.Terminates] : ∃ a, a ∈ s
• Computation.destruct_think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) : s.think.destruct = Sum.inr s
• Computation.equiv_pure_of_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} (h : a ∈ s) : s.Equiv (Computation.pure a)
• Computation.get_eq_of_promises 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] {a : α} : s.Promises a → s.get = a
• Computation.mem_pure_iff 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (a b : α) : a ∈ Computation.pure b ↔ a = b
• Computation.ret_bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (a : α) (f : α → Computation β) : (Computation.pure a).bind f = f a
• Computation.terminates_iff 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) : s.Terminates ↔ ∃ a, a ∈ s
• Computation.Results.mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} {n : ℕ} : s.Results a n → a ∈ s
• Computation.LiftRelAux 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) : α ⊕ Computation α → β ⊕ Computation β → Prop
• Computation.map_pure 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : α → β) (a : α) : Computation.map f (Computation.pure a) = Computation.pure (f a)
• Computation.mem_of_promises 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] {a : α} (p : s.Promises a) : a ∈ s
• Computation.promises_congr 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {c₁ c₂ : Computation α} (h : c₁.Equiv c₂) (a : α) : c₁.Promises a ↔ c₂.Promises a
• Computation.recOn 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {motive : Computation α → Sort v} (s : Computation α) (pure : (a : α) → motive (Computation.pure a)) (think : (s : Computation α) → motive s.think) : motive s
• Computation.Equiv.trans 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s t u : Computation α} : s.Equiv t → t.Equiv u → s.Equiv u
• Computation.eq_thinkN 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} {n : ℕ} (h : s.Results a n) : s = (Computation.pure a).thinkN n
• Computation.exists_results_of_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} (h : a ∈ s) : ∃ n, s.Results a n
• Computation.Results.length 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} {n : ℕ} [_T : s.Terminates] : s.Results a n → s.length = n
• Computation.eq_of_bisim 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (R : Computation α → Computation α → Prop) (bisim : Computation.IsBisimulation R) {s₁ s₂ : Computation α} (r : R s₁ s₂) : s₁ = s₂
• Computation.get_think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] : s.think.get = s.get
• Computation.lift_eq_iff_equiv 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c₁ c₂ : Computation α) : Computation.LiftRel (fun x1 x2 => x1 = x2) c₁ c₂ ↔ c₁.Equiv c₂
• Computation.Results.len_unique 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a b : α} {m n : ℕ} (h1 : s.Results a m) (h2 : s.Results b n) : m = n
• Computation.Results.val_unique 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a b : α} {m n : ℕ} (h1 : s.Results a m) (h2 : s.Results b n) : a = b
• Computation.eq_thinkN' 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [_h : s.Terminates] : s = (Computation.pure s.get).thinkN s.length
• Computation.get_eq_of_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] {a : α} : a ∈ s → s.get = a
• Computation.has_bind_eq_bind 📋 Mathlib.Data.Seq.Computation
  {α β : Type u} (c : Computation α) (f : α → Computation β) : c >>= f = c.bind f
• Computation.mem_of_get_eq 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] {a : α} : s.get = a → a ∈ s
• Computation.of_think_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} : a ∈ s.think → a ∈ s
• Computation.terminates_of_liftRel 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {s : Computation α} {t : Computation β} : Computation.LiftRel R s t → (s.Terminates ↔ t.Terminates)
• Computation.think_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} : a ∈ s → a ∈ s.think
• Computation.map_think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : α → β) (s : Computation α) : Computation.map f s.think = (Computation.map f s).think
• Computation.results_of_terminates' 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [T : s.Terminates] {a : α} (h : a ∈ s) : s.Results a s.length
• Computation.destruct_eq_pure 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} : s.destruct = Sum.inl a → s = Computation.pure a
• Computation.get_thinkN 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] (n : ℕ) : (s.thinkN n).get = s.get
• Computation.liftRel_think_left 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β) : Computation.LiftRel R ca.think cb ↔ Computation.LiftRel R ca cb
• Computation.liftRel_think_right 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β) : Computation.LiftRel R ca cb.think ↔ Computation.LiftRel R ca cb
• Computation.map_congr 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {s1 s2 : Computation α} {f : α → β} (h1 : s1.Equiv s2) : (Computation.map f s1).Equiv (Computation.map f s2)
• Computation.terminatesRecOn 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {C : Computation α → Sort v} (s : Computation α) [s.Terminates] (h1 : (a : α) → C (Computation.pure a)) (h2 : (s : Computation α) → C s → C s.think) : C s
• Computation.terminates_bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (s : Computation α) (f : α → Computation β) [s.Terminates] [(f s.get).Terminates] : (s.bind f).Terminates
• Computation.think_bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (c : Computation α) (f : α → Computation β) : c.think.bind f = (c.bind f).think
• Computation.destruct_eq_think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s s' : Computation α} : s.destruct = Sum.inr s' → s = s'.think
• Computation.empty_orElse 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c : Computation α) : (Computation.empty α <|> c) = c
• Computation.get_equiv 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {c₁ c₂ : Computation α} (h : c₁.Equiv c₂) [c₁.Terminates] [c₂.Terminates] : c₁.get = c₂.get
• Computation.has_map_eq_map 📋 Mathlib.Data.Seq.Computation
  {α β : Type u} (f : α → β) (c : Computation α) : f <$> c = Computation.map f c
• Computation.map_pure' 📋 Mathlib.Data.Seq.Computation
  {α β : Type u_1} (f : α → β) (a : α) : f <$> Computation.pure a = Computation.pure (f a)
• Computation.mem_unique 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a b : α} : a ∈ s → b ∈ s → a = b
• Computation.orElse_empty 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c : Computation α) : (c <|> Computation.empty α) = c
• Computation.thinkN_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} (n : ℕ) : a ∈ s.thinkN n ↔ a ∈ s
• Computation.bind_promises 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {a : α} {b : β} (h1 : s.Promises a) (h2 : (f a).Promises b) : (s.bind f).Promises b
• Computation.bind_pure 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : α → β) (s : Computation α) : s.bind (Computation.pure ∘ f) = Computation.map f s
• Computation.equiv_of_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s t : Computation α} {a : α} (h1 : a ∈ s) (h2 : a ∈ t) : s.Equiv t
• Computation.results_thinkN 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} {m : ℕ} (n : ℕ) : s.Results a m → (s.thinkN n).Results a (m + n)
• Computation.mem_map 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : α → β) {a : α} {s : Computation α} (m : a ∈ s) : f a ∈ Computation.map f s
• Computation.LiftRel.swap 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β) : Computation.LiftRel (Function.swap R) cb ca ↔ Computation.LiftRel R ca cb
• Computation.memRecOn 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {C : Computation α → Sort v} {a : α} {s : Computation α} (M : a ∈ s) (h1 : C (Computation.pure a)) (h2 : (s : Computation α) → C s → C s.think) : C s
• Computation.results_think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} {n : ℕ} (h : s.Results a n) : s.think.Results a (n + 1)
• Computation.ret_orElse 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (a : α) (c₂ : Computation α) : (Computation.pure a <|> c₂) = Computation.pure a
• Computation.corec_eq 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : β → α ⊕ β) (b : β) : (Computation.corec f b).destruct = Computation.rmap (Computation.corec f) (f b)
• Computation.results_think_iff 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} {n : ℕ} : s.think.Results a (n + 1) ↔ s.Results a n
• Computation.map_comp 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (s : Computation α) : Computation.map (g ∘ f) s = Computation.map g (Computation.map f s)
• Computation.orElse_pure 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c₁ : Computation α) (a : α) : (c₁.think <|> Computation.pure a) = Computation.pure a
• Computation.length_thinkN 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [_h : s.Terminates] (n : ℕ) : (s.thinkN n).length = s.length + n
• Computation.liftRelAux_inl_inl 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {a : α} {b : β} : Computation.LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b
• Computation.liftRel_pure_left 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (cb : Computation β) : Computation.LiftRel R (Computation.pure a) cb ↔ ∃ b ∈ cb, R a b
• Computation.liftRel_pure_right 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (b : β) : Computation.LiftRel R ca (Computation.pure b) ↔ ∃ a ∈ ca, R a b
• Computation.LiftRel.imp 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R S : α → β → Prop} (H : ∀ {a : α} {b : β}, R a b → S a b) (s : Computation α) (t : Computation β) : Computation.LiftRel R s t → Computation.LiftRel S s t
• Computation.length_think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) [h : s.Terminates] : s.think.length = s.length + 1
• Computation.bind_assoc 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {γ : Type w} (s : Computation α) (f : α → Computation β) (g : β → Computation γ) : (s.bind f).bind g = s.bind fun x => (f x).bind g
• Computation.liftRelAux_inr_inr 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {ca : Computation α} {cb : Computation β} : Computation.LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb
• Computation.liftRel_congr 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {ca ca' : Computation α} {cb cb' : Computation β} (ha : ca.Equiv ca') (hb : cb.Equiv cb') : Computation.LiftRel R ca cb ↔ Computation.LiftRel R ca' cb'
• Computation.bind_congr 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {s1 s2 : Computation α} {f1 f2 : α → Computation β} (h1 : s1.Equiv s2) (h2 : ∀ (a : α), (f1 a).Equiv (f2 a)) : (s1.bind f1).Equiv (s2.bind f2)
• Computation.map_think' 📋 Mathlib.Data.Seq.Computation
  {α β : Type u_1} (f : α → β) (s : Computation α) : f <$> s.think = (f <$> s).think
• Computation.exists_of_mem_map 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {f : α → β} {b : β} {s : Computation α} (h : b ∈ Computation.map f s) : ∃ a ∈ s, f a = b
• Computation.liftRel_of_mem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {a : α} {b : β} {ca : Computation α} {cb : Computation β} (ma : a ∈ ca) (mb : b ∈ cb) (ab : R a b) : Computation.LiftRel R ca cb
• Computation.rel_of_liftRel 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β} : Computation.LiftRel R ca cb → ∀ {a : α} {b : β}, a ∈ ca → b ∈ cb → R a b
• Computation.destruct_map 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (f : α → β) (s : Computation α) : (Computation.map f s).destruct = Computation.lmap f (Computation.rmap (Computation.map f) s.destruct)
• Computation.of_results_think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {s : Computation α} {a : α} {n : ℕ} (h : s.think.Results a n) : ∃ m, s.Results a m ∧ n = m + 1
• Computation.mem_bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {a : α} {b : β} (h1 : a ∈ s) (h2 : b ∈ f a) : b ∈ s.bind f
• Computation.exists_of_liftRel_left 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β} (H : Computation.LiftRel R ca cb) {a : α} (h : a ∈ ca) : ∃ b ∈ cb, R a b
• Computation.exists_of_liftRel_right 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β} (H : Computation.LiftRel R ca cb) {b : β} (h : b ∈ cb) : ∃ a ∈ ca, R a b
• Computation.results_bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {a : α} {b : β} {m n : ℕ} (h1 : s.Results a m) (h2 : (f a).Results b n) : (s.bind f).Results b (n + m)
• Computation.exists_of_mem_bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {b : β} (h : b ∈ s.bind f) : ∃ a ∈ s, b ∈ f a
• Computation.get_bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (s : Computation α) (f : α → Computation β) [s.Terminates] [(f s.get).Terminates] : (s.bind f).get = (f s.get).get
• Computation.liftRel_rec 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} (C : Computation α → Computation β → Prop) (H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → Computation.LiftRelAux R C ca.destruct cb.destruct) (ca : Computation α) (cb : Computation β) (Hc : C ca cb) : Computation.LiftRel R ca cb
• Computation.LiftRelAux.ret_left 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a : α) (cb : Computation β) : Computation.LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ b ∈ cb, R a b
• Computation.LiftRelAux.ret_right 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (b : β) (ca : Computation α) : Computation.LiftRelAux R C ca.destruct (Sum.inl b) ↔ ∃ a ∈ ca, R a b
• Computation.liftRelAux_inl_inr 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {a : α} {cb : Computation β} : Computation.LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ b ∈ cb, R a b
• Computation.liftRelAux_inr_inl 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {b : β} {ca : Computation α} : Computation.LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ a ∈ ca, R a b
• Computation.liftRel_def 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β} : Computation.LiftRel R ca cb ↔ (ca.Terminates ↔ cb.Terminates) ∧ ∀ {a : α} {b : β}, a ∈ ca → b ∈ cb → R a b
• Computation.liftRel_mem_cases 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β} (Ha : ∀ a ∈ ca, Computation.LiftRel R ca cb) (Hb : ∀ b ∈ cb, Computation.LiftRel R ca cb) : Computation.LiftRel R ca cb
• Computation.liftRel_map 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α} {s2 : Computation β} {f1 : α → γ} {f2 : β → δ} (h1 : Computation.LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)) : Computation.LiftRel S (Computation.map f1 s1) (Computation.map f2 s2)
• Computation.orElse_think 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (c₁ c₂ : Computation α) : (c₁.think <|> c₂.think) = (c₁ <|> c₂).think
• Computation.LiftRelAux.swap 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a : α ⊕ Computation α) (b : β ⊕ Computation β) : Computation.LiftRelAux (Function.swap R) (Function.swap C) b a = Computation.LiftRelAux R C a b
• Computation.LiftRelRec.lem 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {R : α → β → Prop} (C : Computation α → Computation β → Prop) (H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → Computation.LiftRelAux R C ca.destruct cb.destruct) (ca : Computation α) (cb : Computation β) (Hc : C ca cb) (a : α) (ha : a ∈ ca) : Computation.LiftRel R ca cb
• Computation.length_bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (s : Computation α) (f : α → Computation β) [_T1 : s.Terminates] [_T2 : (f s.get).Terminates] : (s.bind f).length = (f s.get).length + s.length
• Computation.of_results_bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {b : β} {k : ℕ} : (s.bind f).Results b k → ∃ a m n, s.Results a m ∧ (f a).Results b n ∧ k = n + m
• Computation.liftRel_bind 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α} {s2 : Computation β} {f1 : α → Computation γ} {f2 : β → Computation δ} (h1 : Computation.LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a b → Computation.LiftRel S (f1 a) (f2 b)) : Computation.LiftRel S (s1.bind f1) (s2.bind f2)
• Computation.terminates_def 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) : s.Terminates ↔ ∃ n, (↑s n).isSome = true
• Computation.le_stable 📋 Mathlib.Data.Seq.Computation
  {α : Type u} (s : Computation α) {a : α} {m n : ℕ} (h : m ≤ n) : ↑s m = some a → ↑s n = some a
• Stream'.Seq.toList' 📋 Mathlib.Data.Seq.Defs
  {α : Type u_1} (s : Stream'.Seq α) : Computation (List α)
• Stream'.WSeq.flatten 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} : Computation (Stream'.WSeq α) → Stream'.WSeq α
• Stream'.WSeq.head 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s : Stream'.WSeq α) : Computation (Option α)
• Stream'.WSeq.toList 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s : Stream'.WSeq α) : Computation (List α)
• Stream'.WSeq.get? 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s : Stream'.WSeq α) (n : ℕ) : Computation (Option α)
• Stream'.WSeq.destruct 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} : Stream'.WSeq α → Computation (Option (α × Stream'.WSeq α))
• Stream'.WSeq.tail.aux 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} : Option (α × Stream'.WSeq α) → Computation (Option (α × Stream'.WSeq α))
• Stream'.WSeq.drop.aux 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} : ℕ → Option (α × Stream'.WSeq α) → Computation (Option (α × Stream'.WSeq α))
• Stream'.WSeq.head_nil 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} : Stream'.WSeq.nil.head = Computation.pure none
• Stream'.WSeq.toList_nil 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} : Stream'.WSeq.nil.toList = Computation.pure []
• Stream'.WSeq.destruct_append.aux 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (t : Stream'.WSeq α) : Option (α × Stream'.WSeq α) → Computation (Option (α × Stream'.WSeq α))
• Stream'.WSeq.destruct_join.aux 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} : Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α)) → Computation (Option (α × Stream'.WSeq α))
• Stream'.WSeq.flatten_think 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (c : Computation (Stream'.WSeq α)) : Stream'.WSeq.flatten c.think = (Stream'.WSeq.flatten c).think
• Stream'.WSeq.head_ofSeq 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s : Stream'.Seq α) : (↑s).head = Computation.pure s.head
• Stream'.WSeq.head_think 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s : Stream'.WSeq α) : s.think.head = s.head.think
• Stream'.WSeq.toList_ofList 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (l : List α) : l ∈ (↑l).toList
• Stream'.WSeq.head_cons 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (a : α) (s : Stream'.WSeq α) : (Stream'.WSeq.cons a s).head = Computation.pure (some a)
• Stream'.WSeq.get?_ofSeq 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s : Stream'.Seq α) (n : ℕ) : (↑s).get? n = Computation.pure (s.get? n)
• Stream'.WSeq.destruct_nil 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} : Stream'.WSeq.nil.destruct = Computation.pure none
• Stream'.WSeq.destruct_think 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s : Stream'.WSeq α) : s.think.destruct = s.destruct.think
• Stream'.WSeq.get?_add 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s : Stream'.WSeq α) (m n : ℕ) : s.get? (m + n) = (s.drop m).get? n
• Stream'.WSeq.drop.aux_none 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (n : ℕ) : Stream'.WSeq.drop.aux n none = Computation.pure none
• Stream'.WSeq.destruct_flatten 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (c : Computation (Stream'.WSeq α)) : (Stream'.WSeq.flatten c).destruct = c >>= Stream'.WSeq.destruct
• Stream'.WSeq.get?_mem 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} {s : Stream'.WSeq α} {a : α} {n : ℕ} : some a ∈ s.get? n → a ∈ s
• Stream'.WSeq.get?_tail 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s : Stream'.WSeq α) (n : ℕ) : s.tail.get? n = s.get? (n + 1)
• Stream'.WSeq.exists_get?_of_mem 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} {s : Stream'.WSeq α} {a : α} (h : a ∈ s) : ∃ n, some a ∈ s.get? n
• Stream'.WSeq.destruct_tail 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s : Stream'.WSeq α) : s.tail.destruct = s.destruct >>= Stream'.WSeq.tail.aux
• Stream'.WSeq.destruct_cons 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (a : α) (s : Stream'.WSeq α) : (Stream'.WSeq.cons a s).destruct = Computation.pure (some (a, s))
• Stream'.WSeq.toList_cons 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (a : α) (s : Stream'.WSeq α) : (Stream'.WSeq.cons a s).toList = (List.cons a <$> s.toList).think
• Stream'.WSeq.destruct_append 📋 Mathlib.Data.WSeq.Basic
  {α : Type u} (s t : Stream'.WSeq α) : (s.append t).destruct = s.destruct.bind (Stream'.WSeq.destruct_append.aux t)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c