Notation for while and repeat loops.

repeat and while notation

inductive Lean.Loop : Type

• mk: Lean.Loop

@[inline]

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

@[specialize #[]]

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

instance Lean.instForInLoopUnit {m : Type u_1 → Type u_2} : ForIn m Lean.Loop Unit

Equations

• Lean.instForInLoopUnit = { forIn := fun {β : Type ?u.14} [Monad m] => Lean.Loop.forIn }

def Lean.doElemRepeat_ : Lean.ParserDescr

def Lean.«doElemWhile_:_Do_» : Lean.ParserDescr

def Lean.doElemWhile_Do_ : Lean.ParserDescr

Equations

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

def Lean.doElemRepeat__Until_ : Lean.ParserDescr