Notation for while and repeat loops.

repeat and while notation

inductive Lean.Loop : Type

• mk : Loop

@[inline]

def Lean.Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] : 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 Loop Unit

def Lean.doElemRepeat_ : ParserDescr

def Lean.«doElemWhile_:_Do_» : ParserDescr

def Lean.doElemWhile_Do_ : ParserDescr

def Lean.doElemRepeat__Until_ : ParserDescr