mathlib documentation

data.mllist

meta inductive tactic.mllist (m : Type uType u) (α : Type u) :
Type u
meta def tactic.mllist.fix {α : Type u} {m : Type uType u} [alternative m] (f : α → m α) :
α → tactic.mllist m α
meta def tactic.mllist.fixl_with {α β : Type u} {m : Type uType u} [alternative m] [monad m] (f : α → m × list β)) :
α → list βtactic.mllist m β
meta def tactic.mllist.fixl {α β : Type u} {m : Type uType u} [alternative m] [monad m] (f : α → m × list β)) (s : α) :
meta def tactic.mllist.uncons {m : Type uType u} [alternative m] [monad m] {α : Type u} :
tactic.mllist m αm (option × tactic.mllist m α))
meta def tactic.mllist.empty {m : Type uType u} [alternative m] [monad m] {α : Type u} (xs : tactic.mllist m α) :
meta def tactic.mllist.of_list {m : Type uType u} [alternative m] [monad m] {α : Type u} :
list αtactic.mllist m α
meta def tactic.mllist.m_of_list {m : Type uType u} [alternative m] [monad m] {α : Type u} :
list (m α)tactic.mllist m α
meta def tactic.mllist.force {m : Type uType u} [alternative m] [monad m] {α : Type u} :
tactic.mllist m αm (list α)
meta def tactic.mllist.take {m : Type uType u} [alternative m] [monad m] {α : Type u} :
tactic.mllist m αm (list α)
meta def tactic.mllist.map {m : Type uType u} [alternative m] [monad m] {α β : Type u} (f : α → β) :
meta def tactic.mllist.mmap {m : Type uType u} [alternative m] [monad m] {α β : Type u} (f : α → m β) :
meta def tactic.mllist.filter {m : Type uType u} [alternative m] [monad m] {α : Type u} (p : α → Prop) [decidable_pred p] :
meta def tactic.mllist.mfilter {m : Type uType u} [alternative m] [monad m] [alternative m] {α β : Type u} (p : α → m β) :
meta def tactic.mllist.filter_map {m : Type uType u} [alternative m] [monad m] {α β : Type u} (f : α → option β) :
meta def tactic.mllist.mfilter_map {m : Type uType u} [alternative m] [monad m] [alternative m] {α β : Type u} (f : α → m β) :
meta def tactic.mllist.append {m : Type uType u} [alternative m] [monad m] {α : Type u} :
meta def tactic.mllist.join {m : Type uType u} [alternative m] [monad m] {α : Type u} :
meta def tactic.mllist.squash {m : Type uType u} [alternative m] [monad m] {α : Type u} (t : m (tactic.mllist m α)) :
meta def tactic.mllist.enum_from {m : Type uType u} [alternative m] [monad m] {α : Type u} :
tactic.mllist m αtactic.mllist m ( × α)
meta def tactic.mllist.enum {m : Type uType u} [alternative m] [monad m] {α : Type u} :
meta def tactic.mllist.range {m : Type → Type} [alternative m] :
meta def tactic.mllist.concat {m : Type uType u} [alternative m] [monad m] {α : Type u} :
tactic.mllist m αα → tactic.mllist m α
meta def tactic.mllist.bind_ {m : Type uType u} [alternative m] [monad m] {α β : Type u} :
tactic.mllist m α(α → tactic.mllist m β)tactic.mllist m β
meta def tactic.mllist.monad_lift {m : Type uType u} [alternative m] [monad m] {α : Type u} (x : m α) :
meta def tactic.mllist.head {m : Type uType u} [alternative m] [monad m] [alternative m] {α : Type u} (L : tactic.mllist m α) :
m α
meta def tactic.mllist.mfirst {m : Type uType u} [alternative m] [monad m] [alternative m] {α β : Type u} (L : tactic.mllist m α) (f : α → m β) :
m β