# mathlib3documentation

data.mllist

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

An alternative construction of lazy lists (see also data.lazy_list), with "lazyness" controlled by an arbitrary monad.

The inductive construction is not allowed outside of meta (indeed, we can build infinite objects). This isn't so bad, as the typical use is with the tactic monad, in any case.

As we're in meta anyway, we don't bother with proofs about these constructions.

meta inductive tactic.mllist (m : Type u Type u) (α : Type u) :

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

Construct an mllist recursively.

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

Repeatedly apply a function f : α → m (α × list β) to an initial a : α, accumulating the elements of the resulting list β as a single monadic lazy list.

(This variant allows starting with a specified list β of elements, as well. )

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

Repeatedly apply a function f : α → m (α × list β) to an initial a : α, accumulating the elements of the resulting list β as a single monadic lazy list.

meta def tactic.mllist.uncons {m : Type u Type u} [monad m] {α : Type u} :
m (option × α))

Deconstruct an mllist, returning inside the monad an optional pair α × mllist m α representing the head and tail of the list.

meta def tactic.mllist.empty {m : Type u Type u} [monad m] {α : Type u} (xs : α) :
m

Compute, inside the monad, whether an mllist is empty.

meta def tactic.mllist.of_list {m : Type u Type u} [monad m] {α : Type u} :
list α

Convert a list to an mllist.

meta def tactic.mllist.m_of_list {m : Type u Type u} [monad m] {α : Type u} :
list (m α)

Convert a list of values inside the monad into an mllist.

meta def tactic.mllist.force {m : Type u Type u} [monad m] {α : Type u} :
m (list α)

Extract a list inside the monad from an mllist.

meta def tactic.mllist.take {m : Type u Type u} [monad m] {α : Type u} :
m (list α)

Take the first n elements, as a list inside the monad.

meta def tactic.mllist.map {m : Type u Type u} [monad m] {α β : Type u} (f : α β) :

Apply a function to every element of an mllist.

meta def tactic.mllist.mmap {m : Type u Type u} [monad m] {α β : Type u} (f : α m β) :

Apply a function which returns values in the monad to every element of an mllist.

meta def tactic.mllist.filter {m : Type u Type u} [monad m] {α : Type u} (p : α Prop)  :

Filter a mllist.

meta def tactic.mllist.mfilter {m : Type u Type u} [monad m] [alternative m] {α β : Type u} (p : α m β) :

Filter a mllist using a function which returns values in the (alternative) monad. Whenever the function "succeeds", we accept the element, and reject otherwise.

meta def tactic.mllist.filter_map {m : Type u Type u} [monad m] {α β : Type u} (f : α ) :

Filter and transform a mllist using an option valued function.

meta def tactic.mllist.mfilter_map {m : Type u Type u} [monad m] [alternative m] {α β : Type u} (f : α m β) :

Filter and transform a mllist using a function that returns values inside the monad. We discard elements where the function fails.

meta def tactic.mllist.append {m : Type u Type u} [monad m] {α : Type u} :

meta def tactic.mllist.join {m : Type u Type u} [monad m] {α : Type u} :
α)

meta def tactic.mllist.squash {m : Type u Type u} [monad m] {α : Type u} (t : m α)) :

meta def tactic.mllist.enum_from {m : Type u Type u} [monad m] {α : Type u} :

Enumerate the elements of a monadic lazy list, starting at a specified offset.

meta def tactic.mllist.enum {m : Type u Type u} [monad m] {α : Type u} :
( × α)

Enumerate the elements of a monadic lazy list.

meta def tactic.mllist.range {m : Type Type} [alternative m] :

The infinite monadic lazy list of natural numbers.

meta def tactic.mllist.concat {m : Type u Type u} [monad m] {α : Type u} :
α

meta def tactic.mllist.bind_ {m : Type u Type u} [monad m] {α β : Type u} :
β)

Apply a function returning a monadic lazy list to each element of a monadic lazy list, joining the results.

meta def tactic.mllist.monad_lift {m : Type u Type u} [monad m] {α : Type u} (x : m α) :

Convert any value in the monad to the singleton monadic lazy list.

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