Documentation

Init.Data.FloatArray.Basic

structure FloatArray :
Instances For
    @[extern lean_mk_empty_float_array]
    Equations
    Instances For
      @[extern lean_float_array_push]
      Equations
      Instances For
        @[extern lean_float_array_size]
        Equations
        Instances For
          @[extern lean_float_array_uget]
          Equations
          Instances For
            @[extern lean_float_array_fget]
            Equations
            Instances For
              @[extern lean_float_array_get]
              Equations
              Instances For
                Equations
                Instances For
                  @[extern lean_float_array_uset]
                  Equations
                  Instances For
                    @[extern lean_float_array_fset]
                    Equations
                    Instances For
                      @[extern lean_float_array_set]
                      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.

                        Equations
                        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 β
                          Equations
                          • One or more equations did not get rendered due to their size.
                          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 FloatArray.size as) (b : β) :
                              m β
                              Equations
                              Instances For
                                Equations
                                • FloatArray.instForInFloatArrayFloat = { forIn := fun {β} [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 (FloatArray.size as)) :
                                m β

                                See comment at forInUnsafe

                                Equations
                                • One or more equations did not get rendered due to their size.
                                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 β
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  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 (FloatArray.size as)) :
                                    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 FloatArray.size as) (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 (FloatArray.size as)) :
                                        β
                                        Equations
                                        Instances For