repeatM

repeatM f a iterates f : α → m (α ⊕ β), recursing on .inl and terminating on .inr.

@[reducible, inline]

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

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

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

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

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

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 β

@[instance_reducible]

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