mathlib documentation

data.mllist

meta inductive tactic.mllist  :
(Type uType u)Type uType u

meta def tactic.mllist.fix {α : Type u} {m : Type uType u} [alternative m] :
(α → m α)α → tactic.mllist m α

meta def tactic.mllist.fixl_with {α β : Type u} {m : Type uType u} [alternative m] [monad m] :
(α → m × list β))α → list βtactic.mllist m β

meta def tactic.mllist.fixl {α β : Type u} {m : Type uType u} [alternative m] [monad m] :
(α → m × list β))α → tactic.mllist m β

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} :
tactic.mllist m αm (ulift bool)

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} :
(α → β)tactic.mllist m αtactic.mllist m β

meta def tactic.mllist.mmap {m : Type uType u} [alternative m] [monad m] {α β : Type u} :
(α → m β)tactic.mllist m αtactic.mllist 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} :
(α → m β)tactic.mllist m αtactic.mllist m α

meta def tactic.mllist.filter_map {m : Type uType u} [alternative m] [monad m] {α β : Type u} :
(α → option β)tactic.mllist m αtactic.mllist m β

meta def tactic.mllist.mfilter_map {m : Type uType u} [alternative m] [monad m] [alternative m] {α β : Type u} :
(α → m β)tactic.mllist m αtactic.mllist 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} :
m (tactic.mllist 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} :
m αtactic.mllist m α

meta def tactic.mllist.head {m : Type uType u} [alternative m] [monad m] [alternative m] {α : Type u} :
tactic.mllist m αm α

meta def tactic.mllist.mfirst {m : Type uType u} [alternative m] [monad m] [alternative m] {α β : Type u} :
tactic.mllist m α(α → m β)m β