Order-theoretic unfolding for whileM #
This module exposes the user-facing one-step unfolding lemma whileM_eq_of_monadTail,
which holds for any monad with a Lean.Order.MonadTail instance. It works by exhibiting
the order-theoretic least fixed point Lean.Order.fix (whileM.body f) and feeding it to
the module-internal whileM_eq.
The lemma does not appear in Init.While itself to keep that module's import closure
small; clients that want to unfold whileM/Loop.forIn should import this file.
theorem
whileM_eq_of_monadTail
{α : Type u}
{m : Type u → Type v}
[Monad m]
{β : Type u}
[Lean.Order.MonadTail m]
[Nonempty β]
{f : α → m (α ⊕ β)}
(a : α)
:
One-step unfolding of whileM 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.