Documentation

Init.Data.FloatArray.Basic

structure FloatArray :
Instances For
    @[extern lean_mk_empty_float_array]
    Equations
    Instances For
      @[extern lean_float_array_push]
      Equations
      • { data := ds }.push x = { data := ds.push x }
      Instances For
        @[extern lean_float_array_size]
        Equations
        • { data := ds }.size = ds.size
        Instances For
          @[extern lean_sarray_size]
          Equations
          • a.usize = a.size.toUSize
          Instances For
            @[extern lean_float_array_uget]
            def FloatArray.uget (a : FloatArray) (i : USize) :
            i.toNat < a.sizeFloat
            Equations
            • { data := ds }.uget x✝ x = ds[x✝]
            Instances For
              @[extern lean_float_array_fget]
              def FloatArray.get (ds : FloatArray) :
              Fin ds.sizeFloat
              Equations
              • { data := ds }.get i = ds.get i
              Instances For
                @[extern lean_float_array_get]
                Equations
                • { data := ds }.get! x = ds.get! x
                Instances For
                  Equations
                  • ds.get? i = if h : i < ds.size then some (ds.get i, h) else none
                  Instances For
                    Equations
                    Equations
                    @[extern lean_float_array_uset]
                    def FloatArray.uset (a : FloatArray) (i : USize) :
                    Floati.toNat < a.sizeFloatArray
                    Equations
                    • { data := ds }.uset x✝¹ x✝ x = { data := ds.uset x✝¹ x✝ x }
                    Instances For
                      @[extern lean_float_array_fset]
                      def FloatArray.set (ds : FloatArray) :
                      Fin ds.sizeFloatFloatArray
                      Equations
                      • { data := ds }.set i x = { data := ds.set i x }
                      Instances For
                        @[extern lean_float_array_set]
                        Equations
                        • { data := ds }.set! x✝ x = { data := ds.set! x✝ x }
                        Instances For
                          Equations
                          • s.isEmpty = (s.size == 0)
                          Instances For
                            Equations
                            Instances For
                              @[inline]
                              unsafe def FloatArray.forInUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatArray) (b : β) (f : Floatβm (ForInStep β)) :
                              m β

                              We claim this unsafe implementation is correct because an array cannot have more than usizeSz elements in our runtime. This is similar to the Array version.

                              Instances For
                                @[specialize #[]]
                                unsafe def FloatArray.forInUnsafe.loop {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatArray) (f : Floatβm (ForInStep β)) (sz : USize) (i : USize) (b : β) :
                                m β
                                Instances For
                                  @[implemented_by FloatArray.forInUnsafe]
                                  def FloatArray.forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatArray) (b : β) (f : Floatβm (ForInStep β)) :
                                  m β

                                  Reference implementation for forIn

                                  Equations
                                  Instances For
                                    def FloatArray.forIn.loop {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatArray) (f : Floatβm (ForInStep β)) (i : Nat) (h : i as.size) (b : β) :
                                    m β
                                    Equations
                                    Instances For
                                      Equations
                                      • FloatArray.instForInFloat = { forIn := fun {β : Type ?u.14} [Monad m] => FloatArray.forIn }
                                      @[inline]
                                      unsafe def FloatArray.foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : βFloatm β) (init : β) (as : FloatArray) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                      m β

                                      See comment at forInUnsafe

                                      Instances For
                                        @[specialize #[]]
                                        unsafe def FloatArray.foldlMUnsafe.fold {β : Type v} {m : Type v → Type w} [Monad m] (f : βFloatm β) (as : FloatArray) (i : USize) (stop : USize) (b : β) :
                                        m β
                                        Instances For
                                          @[implemented_by FloatArray.foldlMUnsafe]
                                          def FloatArray.foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : βFloatm β) (init : β) (as : FloatArray) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                          m β

                                          Reference implementation for foldlM

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def FloatArray.foldlM.loop {β : Type v} {m : Type v → Type w} [Monad m] (f : βFloatm β) (as : FloatArray) (stop : Nat) (h : stop as.size) (i : Nat) (j : Nat) (b : β) :
                                            m β
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[inline]
                                              def FloatArray.foldl {β : Type v} (f : βFloatβ) (init : β) (as : FloatArray) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                              β
                                              Equations
                                              Instances For
                                                Equations
                                                Instances For
                                                  Equations