- 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] :
(α → m α) → α → tactic.mllist m α
def
tactic.mllist.fixl_with
{α β : Type u}
{m : Type u → Type u}
[alternative m]
[monad m] :
(α → m (α × list β)) → α → list β → tactic.mllist m β
def
tactic.mllist.fixl
{α β : Type u}
{m : Type u → Type u}
[alternative m]
[monad m] :
(α → m (α × list β)) → α → tactic.mllist m β
def
tactic.mllist.uncons
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
tactic.mllist m α → m (option (α × tactic.mllist m α))
def
tactic.mllist.empty
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
tactic.mllist m α → m (ulift bool)
def
tactic.mllist.of_list
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
list α → tactic.mllist m α
def
tactic.mllist.m_of_list
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
list (m α) → tactic.mllist m α
def
tactic.mllist.force
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
tactic.mllist m α → m (list α)
def
tactic.mllist.take
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
tactic.mllist m α → ℕ → m (list α)
def
tactic.mllist.map
{m : Type u → Type u}
[alternative m]
[monad m]
{α β : Type u} :
(α → β) → tactic.mllist m α → tactic.mllist m β
def
tactic.mllist.mmap
{m : Type u → Type u}
[alternative m]
[monad m]
{α β : Type u} :
(α → m β) → 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] :
tactic.mllist m α → tactic.mllist m α
def
tactic.mllist.mfilter
{m : Type u → Type u}
[alternative m]
[monad m]
[alternative m]
{α β : Type u} :
(α → m β) → tactic.mllist m α → tactic.mllist m α
def
tactic.mllist.filter_map
{m : Type u → Type u}
[alternative m]
[monad m]
{α β : Type u} :
(α → option β) → tactic.mllist m α → tactic.mllist m β
def
tactic.mllist.mfilter_map
{m : Type u → Type u}
[alternative m]
[monad m]
[alternative m]
{α β : Type u} :
(α → m β) → tactic.mllist m α → tactic.mllist m β
def
tactic.mllist.append
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
tactic.mllist m α → tactic.mllist m α → tactic.mllist m α
def
tactic.mllist.join
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
tactic.mllist m (tactic.mllist m α) → tactic.mllist m α
def
tactic.mllist.squash
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
m (tactic.mllist m α) → tactic.mllist m α
def
tactic.mllist.enum_from
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
ℕ → tactic.mllist m α → tactic.mllist m (ℕ × α)
def
tactic.mllist.enum
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
tactic.mllist m α → tactic.mllist m (ℕ × α)
def
tactic.mllist.concat
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
tactic.mllist m α → α → tactic.mllist m α
def
tactic.mllist.bind_
{m : Type u → Type u}
[alternative m]
[monad m]
{α β : Type u} :
tactic.mllist m α → (α → tactic.mllist m β) → tactic.mllist m β
def
tactic.mllist.monad_lift
{m : Type u → Type u}
[alternative m]
[monad m]
{α : Type u} :
m α → tactic.mllist m α
def
tactic.mllist.head
{m : Type u → Type u}
[alternative m]
[monad m]
[alternative m]
{α : Type u} :
tactic.mllist m α → m α
def
tactic.mllist.mfirst
{m : Type u → Type u}
[alternative m]
[monad m]
[alternative m]
{α β : Type u} :
tactic.mllist m α → (α → m β) → m β