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

@[implicit_reducible]

instance Lean.Order.instMonadTailId : MonadTail Id

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• Lean.Order.instMonadTailExceptT = { instCCPO := fun (β : Type ?u.2) [Nonempty β] => Lean.Order.MonadTail.instCCPO (Except ε β), bind_mono_right := ⋯ }

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• Lean.Order.instMonadTailOptionT = { instCCPO := fun (β : Type ?u.2) [Nonempty β] => Lean.Order.MonadTail.instCCPO (Option β), bind_mono_right := ⋯ }

@[implicit_reducible]

instance Lean.Order.instMonadTailOption : MonadTail Option

Equations

• Lean.Order.instMonadTailOption = { instCCPO := fun (x : Type ?u.1) [Nonempty x] => inferInstance, bind_mono_right := @Lean.Order.instMonadTailOption._proof_1 }

@[implicit_reducible]

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

Equations

• Lean.Order.instMonadTailReaderT = { instCCPO := fun (α : Type ?u.2) [Nonempty α] => { toPartialOrder := Lean.Order.instPartialOrderReaderT, has_csup := ⋯ }, bind_mono_right := ⋯ }

noncomputable def Lean.Order.ST.bot' {α σ : Type} [Nonempty α] (s : Void σ) : FlatOrder { val := Classical.ofNonempty, state := Classical.choice ⋯ }

Equations

• Lean.Order.ST.bot' s = { val := Classical.ofNonempty, state := Classical.choice ⋯ }

@[implicit_reducible]

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

Equations

• Lean.Order.instCCPOSTOfNonempty = { rel := Lean.Order.PartialOrder.rel, rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯, has_csup := ⋯ }

@[implicit_reducible]

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

Equations

• Lean.Order.instMonadTailST = { instCCPO := fun (x : Type) [Nonempty x] => inferInstance, bind_mono_right := ⋯ }

@[implicit_reducible]

instance Lean.Order.instMonadTailBaseIO : MonadTail BaseIO

Equations

• Lean.Order.instMonadTailBaseIO = { instCCPO := Lean.Order.instMonadTailBaseIO._aux_1, bind_mono_right := @Lean.Order.instMonadTailBaseIO._proof_3 }

@[implicit_reducible]

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

Equations

• Lean.Order.instMonadTailESTOfNonempty = { instCCPO := fun (x : Type) [Nonempty x] => inferInstance, bind_mono_right := ⋯ }

@[implicit_reducible]

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

Equations

• Lean.Order.instMonadTailEIOOfNonempty = { instCCPO := fun (β : Type) [Nonempty β] => Lean.Order.instCCPOEIOOfNonempty, bind_mono_right := ⋯ }

@[implicit_reducible]

instance Lean.Order.instMonadTailIO : MonadTail IO

Equations

• Lean.Order.instMonadTailIO = { instCCPO := fun (β : Type) [Nonempty β] => Lean.Order.instCCPOIO, bind_mono_right := @Lean.Order.instMonadTailIO._proof_1 }

@[implicit_reducible]

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

Equations

• Lean.Order.instMonadTailStateRefT' = { instCCPO := Lean.Order.instMonadTailStateRefT'._aux_1, bind_mono_right := ⋯ }