Documentation

Init.Data.Range.Basic

source
structure Std.Legacy.Range :
Type
Instances For
    source
    @[implicit_reducible]
    instance Std.Legacy.instMembershipNatRange :
    Membership Nat Range
    source
    def Std.Legacy.Range.size (r : Range) :
    Nat

    The number of elements in the range.

    Instances For
      source
      @[inline]
      def Std.Legacy.Range.forIn' {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (range : Range) (init : β) (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) :
      m β
      Instances For
        source
        @[implicit_reducible]
        instance Std.Legacy.Range.instForIn'NatInferInstanceMembershipOfMonad {m : Type u_1 → Type u_2} [Monad m] :
        ForIn' m Range Nat inferInstance
        source
        @[inline]
        def Std.Legacy.Range.forM {m : Type u_1 → Type u_2} [Monad m] (range : Range) (f : Nat → m PUnit) :
        m PUnit
        Instances For
          source
          @[implicit_reducible]
          instance Std.Legacy.Range.instForMNatOfMonad {m : Type u_1 → Type u_2} [Monad m] :
          ForM m Range Nat
          source
          def Std.Legacy.Range.«term[:_]» :
          Lean.ParserDescr
          Instances For
            source
            def Std.Legacy.Range.«term[_:_]» :
            Lean.ParserDescr
            Instances For
              source
              def Std.Legacy.Range.«term[:_:_]» :
              Lean.ParserDescr
              Instances For
                source
                def Std.Legacy.Range.«term[_:_:_]» :
                Lean.ParserDescr
                Instances For
                  source
                  theorem Membership.mem.upper {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) :
                  i < r.stop
                  source
                  theorem Membership.mem.lower {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) :
                  r.start ≤ i
                  source
                  theorem Membership.mem.step {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) :
                  (i - r.start) % r.step = 0
                  source
                  theorem Membership.get_elem_helper {i n : Nat} {r : Std.Legacy.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) :
                  i < n