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 β

Equations

• x✝.forIn init f = Lean.Loop.forIn.loop f init

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

Equations

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

def Lean.doElemRepeat_ : ParserDescr

Equations

• Lean.doElemRepeat_ = Lean.ParserDescr.node `Lean.doElemRepeat_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "repeat ") (Lean.ParserDescr.const `doSeq))

def Lean.«doElemWhile_:_Do_» : ParserDescr

Equations

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

def Lean.doElemWhile_Do_ : ParserDescr

Equations

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

def Lean.doElemRepeat__Until_ : ParserDescr

Equations

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