Order-theoretic unfolding for repeatM

This module proves the one-step unfolding lemma repeatM.Internal.eq_of_monadTail, which holds for any monad with a Lean.Order.MonadTail instance. It exhibits the order-theoretic least fixed point Lean.Order.fix (repeatM.body f) and feeds it to repeatM_eq.

Unfolding repeatM/Lean.Loop.forIn requires importing this module.

theorem repeatM.Internal.eq_of_monadTail {α : Type u} {m : Type u → Type v} [Monad m] {β : Type u} [Lean.Order.MonadTail m] [Nonempty β] {f : α → m (α ⊕ β)} (a : α) : repeatM f a = body f (repeatM f) a

One-step unfolding of repeatM for any MonadTail m.

theorem Lean.Loop.forIn_eq_of_monadTail {m : Type u → Type v} [Monad m] {β : Type u} [LawfulMonad m] [Order.MonadTail m] {l : Loop} {b : β} {f : Unit → β → m (ForInStep β)} : l.forIn b f = do let __do_lift ← f () b match __do_lift with | ForInStep.done val => pure val | ForInStep.yield val => l.forIn val f

One-step unfolding of Lean.Loop.forIn for any MonadTail m.