Documentation

Init.Data.FloatArray.Basic

structure FloatArray :
Type
@[extern lean_mk_empty_float_array]
Equations
@[extern lean_float_array_push]
Equations
@[extern lean_float_array_size]
Equations
@[extern lean_float_array_uget]
Equations
@[extern lean_float_array_fget]
Equations
@[extern lean_float_array_get]
Equations
Equations
@[inline]
def FloatArray.getOp (self : FloatArray) (idx : Nat) :
Equations
@[extern lean_float_array_uset]
Equations
@[extern lean_float_array_fset]
Equations
@[extern lean_float_array_set]
Equations
Equations
partial def FloatArray.toList.loop (ds : FloatArray) (i : Nat) (r : List Float) :
@[inline]
unsafe def FloatArray.forInUnsafe {β : Type v} {m : Type vType w} [inst : Monad m] (as : FloatArray) (b : β) (f : Floatβm (ForInStep β)) :
m β
Equations
@[specialize]
unsafe def FloatArray.forInUnsafe.loop {β : Type v} {m : Type vType w} [inst : Monad m] (as : FloatArray) (f : Floatβm (ForInStep β)) (sz : USize) (i : USize) (b : β) :
m β
Equations
@[implementedBy FloatArray.forInUnsafe]
noncomputable def FloatArray.forIn {β : Type v} {m : Type vType w} [inst : Monad m] (as : FloatArray) (b : β) (f : Floatβm (ForInStep β)) :
m β
Equations
def FloatArray.forIn.loop {β : Type v} {m : Type vType w} [inst : Monad m] (as : FloatArray) (f : Floatβm (ForInStep β)) (i : Nat) (h : i FloatArray.size as) (b : β) :
m β
Equations
instance FloatArray.instForInFloatArrayFloat {m : Type u_1Type u_2} :
Equations
  • FloatArray.instForInFloatArrayFloat = { forIn := fun {β} [Monad m] => FloatArray.forIn }
@[inline]
unsafe def FloatArray.foldlMUnsafe {β : Type v} {m : Type vType w} [inst : Monad m] (f : βFloatm β) (init : β) (as : FloatArray) (start : optParam Nat 0) (stop : optParam Nat (FloatArray.size as)) :
m β
Equations
@[specialize]
unsafe def FloatArray.foldlMUnsafe.fold {β : Type v} {m : Type vType w} [inst : Monad m] (f : βFloatm β) (as : FloatArray) (i : USize) (stop : USize) (b : β) :
m β
Equations
@[implementedBy FloatArray.foldlMUnsafe]
noncomputable def FloatArray.foldlM {β : Type v} {m : Type vType w} [inst : Monad m] (f : βFloatm β) (init : β) (as : FloatArray) (start : optParam Nat 0) (stop : optParam Nat (FloatArray.size as)) :
m β
Equations
def FloatArray.foldlM.loop {β : Type v} {m : Type vType w} [inst : Monad m] (f : βFloatm β) (as : FloatArray) (stop : Nat) (h : stop FloatArray.size as) (i : Nat) (j : Nat) (b : β) :
m β
Equations
@[inline]
def FloatArray.foldl {β : Type v} (f : βFloatβ) (init : β) (as : FloatArray) (start : optParam Nat 0) (stop : optParam Nat (FloatArray.size as)) :
β
Equations