def Lean.Elab.Do.elabDoRepeat : DoElab

Builtin do-element elaborator for repeat (syntax kind Lean.Parser.Term.doRepeat).

Expands to for _ in Loop.mk do .... When the body cannot break, the loop's own expression type is fixed to PUnit, yet the surrounding do block may require a different result type; we append an unreachable! so the continuation has a polymorphic value of any type. The unreachable! is never actually executed (the loop never terminates normally), and any dead-code warning that fires on the surrounding continuation is actionable — the user can remove the following code without breaking the do block's type.

Equations

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

def Lean.Elab.Do.expandDoWhile : Macro

Equations

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

def Lean.Elab.Do.expandDoRepeatUntil : Macro

Equations

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