Documentation

Init.Internal.Order.MonadTail

class Lean.Order.MonadTail (m : Type u → Type v) [Bind m] :

Type (max (u + 1) v)

A tail monad is a monad whose bind operation preserves a chosen ordering of the continuation. Specifically, MonadTail m asserts that every m β carries a chain-complete partial order (CCPO) and that >>= is monotone in its second (continuation) argument with respect to that order.

This is a weaker requirement than MonoBind, which requires monotonicity in both arguments. MonadTail is sufficient for partial_fixpoint-like recursive definitions where the recursive call only appears in the continuation (second argument) of >>=.

instCCPO (β : Type u) [Nonempty β] : CCPO (m β)
Every m β with Nonempty β has a chain-complete partial order.
bind_mono_right {α β : Type u} {a : m α} {f₁ f₂ : α → m β} [Nonempty β] (h : ∀ (x : α), PartialOrder.rel (f₁ x) (f₂ x)) : PartialOrder.rel (a >>= f₁) (a >>= f₂)
Bind is monotone in the second (continuation) argument.

Instances

theorem Lean.Order.MonadTail.monotone_bind_right (m : Type u → Type v) [Monad m] [MonadTail m] {α β : Type u} [Nonempty β] {γ : Sort w} [PartialOrder γ] (f : m α) (g : γ → α → m β) (hmono : monotone g) :

monotone fun (x : γ) => f >>= g x

@[implicit_reducible]

instance Lean.Order.instMonadTailId :

@[implicit_reducible]

instance Lean.Order.instMonadTailStateTOfNonempty {σ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] [Nonempty σ] :

MonadTail (StateT σ m)

@[implicit_reducible]

instance Lean.Order.instMonadTailExceptT {ε : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :

MonadTail (ExceptT ε m)

@[implicit_reducible]

instance Lean.Order.instMonadTailExcept {ε : Type u_1} :

MonadTail (Except ε)

@[implicit_reducible]

instance Lean.Order.instMonadTailOptionT {m : Type u → Type v} [Monad m] [MonadTail m] :

MonadTail (OptionT m)

@[implicit_reducible]

instance Lean.Order.instMonadTailOption :

MonadTail Option

@[implicit_reducible]

instance Lean.Order.instMonadTailReaderT {ρ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :

MonadTail (ReaderT ρ m)

noncomputable def Lean.Order.ST.bot' {α σ : Type} [Nonempty α] (s : Void σ) :

FlatOrder { val := Classical.ofNonempty, state := Classical.choice ⋯ }

Instances For

@[implicit_reducible]

instance Lean.Order.instCCPOSTOfNonempty {α σ : Type} [Nonempty α] :

CCPO (ST σ α)

@[implicit_reducible]

instance Lean.Order.instMonadTailST {σ : Type} :

MonadTail (ST σ)

@[implicit_reducible]

instance Lean.Order.instMonadTailBaseIO :

MonadTail BaseIO

@[implicit_reducible]

instance Lean.Order.instMonadTailESTOfNonempty {ε σ : Type} [Nonempty ε] :

MonadTail (EST ε σ)

@[implicit_reducible]

instance Lean.Order.instMonadTailEIOOfNonempty {ε : Type} [Nonempty ε] :

MonadTail (EIO ε)

@[implicit_reducible]

instance Lean.Order.instMonadTailIO :

@[implicit_reducible]

instance Lean.Order.instMonadTailStateRefT' {ω σ : Type} {m : Type → Type} [Monad m] [MonadTail m] :

MonadTail (StateRefT' ω σ m)