repeatM

repeatM f a iterates f : α → m (α ⊕ β), recursing on .inl and terminating on .inr. The public unfolding lemma repeatM_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 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.

Equations

• repeatM.body f recur a = do let __do_lift ← f a match __do_lift with | Sum.inl a => recur a | Sum.inr b => pure b

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

Its unfolding lemma is repeatM_eq_of_monadTail.

Equations

• repeatM f a = (repeatM.impl✝ f a).val

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 β

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• Lean.instForInLoopUnitOfMonad = { forIn := fun {β : Type ?u.2} => Lean.Loop.forIn }