Documentation

Init.Data.Range

structure Std.Range :
Instances For
    Equations
    @[inline]
    def Std.Range.forIn {β : Type u} {m : Type u → Type v} [Monad m] (range : Std.Range) (init : β) (f : Natβm (ForInStep β)) :
    m β
    Equations
    Instances For
      @[specialize #[]]
      def Std.Range.forIn.loop {β : Type u} {m : Type u → Type v} [Monad m] (f : Natβm (ForInStep β)) (fuel : Nat) (i : Nat) (stop : Nat) (step : Nat) (b : β) :
      m β
      Equations
      Instances For
        instance Std.Range.instForInNat {m : Type u_1 → Type u_2} :
        Equations
        • Std.Range.instForInNat = { forIn := fun {β : Type ?u.14} [Monad m] => Std.Range.forIn }
        @[inline]
        def Std.Range.forIn' {β : Type u} {m : Type u → Type v} [Monad m] (range : Std.Range) (init : β) (f : (i : Nat) → i rangeβm (ForInStep β)) :
        m β
        Equations
        • range.forIn' init f = Std.Range.forIn'.loop range.start range.stop range.step f range.stop range.start init
        Instances For
          @[specialize #[]]
          def Std.Range.forIn'.loop {β : Type u} {m : Type u → Type v} [Monad m] (start : Nat) (stop : Nat) (step : Nat) (f : (i : Nat) → start i i < stopβm (ForInStep β)) (fuel : Nat) (i : Nat) (hl : start i) (b : β) :
          m β
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            instance Std.Range.instForIn'NatInferInstanceMembership {m : Type u_1 → Type u_2} :
            ForIn' m Std.Range Nat inferInstance
            Equations
            • Std.Range.instForIn'NatInferInstanceMembership = { forIn' := fun {β : Type ?u.14} [Monad m] => Std.Range.forIn' }
            @[inline]
            def Std.Range.forM {m : Type u → Type v} [Monad m] (range : Std.Range) (f : Natm PUnit) :
            Equations
            Instances For
              @[specialize #[]]
              def Std.Range.forM.loop {m : Type u → Type v} [Monad m] (f : Natm PUnit) (fuel : Nat) (i : Nat) (stop : Nat) (step : Nat) :
              Equations
              Instances For
                instance Std.Range.instForMNat {m : Type u_1 → Type u_2} :
                Equations
                • Std.Range.instForMNat = { forM := fun [Monad m] => Std.Range.forM }
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i r) :
                        i < r.stop
                        theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i r) :
                        r.start i
                        theorem Membership.get_elem_helper {i : Nat} {n : Nat} {r : Std.Range} (h₁ : i r) (h₂ : r.stop = n) :
                        i < n