mathlib3 documentation

data.mllist

Monadic lazy lists. #

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.

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

A monadic lazy list, controlled by an arbitrary monad.

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

Construct an mllist recursively.

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

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. )

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

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

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

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

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

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

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

Convert a list to an mllist.

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

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

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

Extract a list inside the monad from an mllist.

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

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

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

Apply a function to every element of an mllist.

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

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

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

Filter a mllist.

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

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

Filter and transform a mllist using an option valued function.

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

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

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

Concatenate two monadic lazty lists.

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

Join a monadic lazy list of monadic lazy lists into a single monadic lazy list.

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

Lift a monadic lazy list inside the monad to a monadic lazy list.

source
meta def tactic.mllist.enum_from {m : Type u → Type u} [monad m] {α : Type u} :
ℕ → tactic.mllist m α → tactic.mllist m (ℕ × α)

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

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

Enumerate the elements of a monadic lazy list.

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

The infinite monadic lazy list of natural numbers.

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

Add one element to the end of a monadic lazy list.

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

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

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

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

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

Return the head of a monadic lazy list, as a value in the monad.

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

Apply a function returning values inside the monad to a monadic lazy list, returning only the first successful result.