Init.Data.FloatArray.Basic

FloatArray.uset _fun_discr _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr, _fun_discr with | { data := ds }, i, v, h => { data := Array.uset ds i v h }

source

@[extern lean_float_array_fset]

def FloatArray.set (ds : FloatArray) :

Fin (FloatArray.size ds) → Float → FloatArray

Equations

FloatArray.set _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr with | { data := ds }, i, d => { data := Array.set ds i d }

source

@[extern lean_float_array_set]

def FloatArray.set!:

FloatArray → Nat → Float → FloatArray

Equations

FloatArray.set! _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr with | { data := ds }, i, d => { data := Array.set! ds i d }

source

def FloatArray.isEmpty (s : FloatArray) :

Bool

Equations

FloatArray.isEmpty s = (FloatArray.size s == 0)

source

def FloatArray.toList (ds : FloatArray) :

List Float

Equations

FloatArray.toList ds = FloatArray.toList.loop ds 0 []

source

partial def FloatArray.toList.loop (ds : FloatArray) (i : Nat) (r : List Float) :

List Float

source

@[inline]

unsafe def FloatArray.forInUnsafe {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : FloatArray) (b : β) (f : Float → β → m (ForInStep β)) :

m β

Equations

FloatArray.forInUnsafe as b f = let sz := USize.ofNat (FloatArray.size as); FloatArray.forInUnsafe.loop as f sz 0 b

source

@[specialize]

unsafe def FloatArray.forInUnsafe.loop {β : Type v} {m : Type v → Type w} [inst : 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.

source

@[implementedBy FloatArray.forInUnsafe]

def FloatArray.forIn {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : FloatArray) (b : β) (f : Float → β → m (ForInStep β)) :

m β

Equations

FloatArray.forIn as b f = FloatArray.forIn.loop as f (FloatArray.size as) (_ : FloatArray.size as ≤ FloatArray.size as) b

source

def FloatArray.forIn.loop {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : FloatArray) (f : Float → β → m (ForInStep β)) (i : Nat) (h : i ≤ FloatArray.size as) (b : β) :

m β

Equations

One or more equations did not get rendered due to their size.
FloatArray.forIn.loop as f 0 x b = pure b

source

instance FloatArray.instForInFloatArrayFloat {m : Type u_1 → Type u_2} :

ForIn m FloatArray Float

Equations

FloatArray.instForInFloatArrayFloat = { forIn := fun {β} [Monad m] => FloatArray.forIn }

source

@[inline]

unsafe def FloatArray.foldlMUnsafe {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → Float → m β) (init : β) (as : FloatArray) (start : optParam Nat 0) (stop : optParam Nat (FloatArray.size as)) :

m β

Equations

One or more equations did not get rendered due to their size.

source

@[specialize]

unsafe def FloatArray.foldlMUnsafe.fold {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → Float → m β) (as : FloatArray) (i : USize) (stop : USize) (b : β) :

m β

Equations

One or more equations did not get rendered due to their size.

source

@[implementedBy FloatArray.foldlMUnsafe]

def FloatArray.foldlM {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → Float → m β) (init : β) (as : FloatArray) (start : optParam Nat 0) (stop : optParam Nat (FloatArray.size as)) :

m β

Equations

One or more equations did not get rendered due to their size.

source

def FloatArray.foldlM.loop {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → Float → m β) (as : FloatArray) (stop : Nat) (h : stop ≤ FloatArray.size as) (i : Nat) (j : Nat) (b : β) :

m β

Equations