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