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.

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

@[instance_reducible]

instance Lean.Order.instMonadTailId : MonadTail Id

@[instance_reducible]

instance Lean.Order.instMonadTailStateT {σ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] : MonadTail (StateT σ m)

@[instance_reducible]

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

@[instance_reducible]

instance Lean.Order.instMonadTailExcept {ε : Type u_1} : MonadTail (Except ε)

@[instance_reducible]

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

@[instance_reducible]

instance Lean.Order.instMonadTailOption : MonadTail Option

@[instance_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 ⋯ }

@[instance_reducible]

instance Lean.Order.instCCPOSTOfNonempty {α σ : Type} [Nonempty α] : CCPO (ST σ α)

@[instance_reducible]

instance Lean.Order.instMonadTailST {σ : Type} : MonadTail (ST σ)

@[instance_reducible]

instance Lean.Order.instMonadTailBaseIO : MonadTail BaseIO

@[instance_reducible]

instance Lean.Order.instMonadTailESTOfNonempty {ε σ : Type} [Nonempty ε] : MonadTail (EST ε σ)

@[instance_reducible]

instance Lean.Order.instMonadTailEIOOfNonempty {ε : Type} [Nonempty ε] : MonadTail (EIO ε)

@[instance_reducible]

instance Lean.Order.instMonadTailIO : MonadTail IO

@[instance_reducible]

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