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