whileM

whileM f a iterates f : α → m (α ⊕ β), recursing on .inl and terminating on .inr. The public unfolding lemma whileM_eq_of_monadTail, which requires a Lean.Order.MonadTail m instance, lives in Init.Internal.Order.While to keep this module's import closure small.

@[reducible, inline]

abbrev whileM.body {α : Type u} {m : Type u → Type v} [Monad m] {β : Type u} (f : α → m (α ⊕ β)) (recur : α → m β) (a : α) : m β

The body of whileM: run f a, recurse via recur on .inl, return on .inr.

@[implemented_by _private.Init.While.0.whileM.erased]

def whileM {α : Type u} {m : Type u → Type v} [Monad m] {β : Type u} [Nonempty β] (f : α → m (α ⊕ β)) (a : α) : m β

whileM f a iterates f at a, recursing on .inl and terminating on .inr.

Its unfolding lemma is whileM_eq_of_monadTail.

Loop type backing repeat/while/repeat ... until

The parsers and elaborators for repeat, while, and repeat ... until live in Lean.Parser.Do and Lean.Elab.BuiltinDo.Repeat. This module only provides the Loop type (and ForIn instance) that those elaborators expand to.

structure Lean.Loop : Type

@[inline]

def Lean.Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] : Loop → (init : β) → (f : Unit → β → m (ForInStep β)) → m β

@[implicit_reducible]

instance Lean.instForInLoopUnitOfMonad {m : Type u → Type v} [Monad m] : ForIn m Loop Unit