Documentation

Init.While

Notation for while and repeat loops. #

repeat and while notation #

source
inductive Lean.Loop :
Type
Instances For
    source
    @[inline]
    def Lean.Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] :
    Loop → (init : β) → (f : Unit → β → m (ForInStep β)) → m β
    Instances For
      source
      @[implicit_reducible]
      instance Lean.instForInLoopUnitOfMonad {m : Type u_1 → Type u_2} [Monad m] :
      ForIn m Loop Unit
      source
      def Lean.doElemRepeat_ :
      ParserDescr
      Instances For
        source
        def Lean.«doElemWhile_:_Do_» :
        ParserDescr
        Instances For
          source
          def Lean.doElemWhile_Do_ :
          ParserDescr
          Instances For
            source
            def Lean.doElemRepeat__Until_ :
            ParserDescr
            Instances For