structure FloatArray : Type

• data : Array Float

@[extern lean_mk_empty_float_array]

def FloatArray.emptyWithCapacity (c : Nat) : FloatArray

@[reducible, inline, deprecated FloatArray.emptyWithCapacity (since := "2025-03-12")]

abbrev FloatArray.mkEmpty (c : Nat) : FloatArray

def FloatArray.empty : FloatArray

instance FloatArray.instInhabited : Inhabited FloatArray

instance FloatArray.instEmptyCollection : EmptyCollection FloatArray

@[extern lean_float_array_push]

def FloatArray.push : FloatArray → Float → FloatArray

@[extern lean_float_array_size]

def FloatArray.size : FloatArray → Nat

@[extern lean_sarray_size]

def FloatArray.usize (a : FloatArray) : USize

@[extern lean_float_array_uget]

def FloatArray.uget (a : FloatArray) (i : USize) : i.toNat < a.size → Float

@[extern lean_float_array_fget]

def FloatArray.get (ds : FloatArray) (i : Nat) (h : i < ds.size := by get_elem_tactic) : Float

@[extern lean_float_array_get]

def FloatArray.get! : FloatArray → Nat → Float

def FloatArray.get? (ds : FloatArray) (i : Nat) : Option Float

instance FloatArray.instGetElemNatFloatLtSize : GetElem FloatArray Nat Float fun (xs : FloatArray) (i : Nat) => i < xs.size

instance FloatArray.instGetElemUSizeFloatLtNatToNatSize : GetElem FloatArray USize Float fun (xs : FloatArray) (i : USize) => i.toNat < xs.size

@[extern lean_float_array_uset]

def FloatArray.uset (a : FloatArray) (i : USize) : Float → (h : autoParam (i.toNat < a.size) _auto✝) → FloatArray

@[extern lean_float_array_fset]

def FloatArray.set (ds : FloatArray) (i : Nat) : Float → (h : autoParam (i < ds.size) _auto✝) → FloatArray

@[extern lean_float_array_set]

def FloatArray.set! : FloatArray → Nat → Float → FloatArray

def FloatArray.isEmpty (s : FloatArray) : Bool

def FloatArray.toList (ds : FloatArray) : List Float

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

@[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.

@[specialize #[]]

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

@[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

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 β

instance FloatArray.instForInFloat {m : Type u_1 → Type u_2} : ForIn m FloatArray Float

@[inline]

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

See comment at forInUnsafe

@[specialize #[]]

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

@[implemented_by FloatArray.foldlMUnsafe]

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

Reference implementation for foldlM

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

@[inline]

def FloatArray.foldl {β : Type v} (f : β → Float → β) (init : β) (as : FloatArray) (start : Nat := 0) (stop : Nat := as.size) : β

def List.toFloatArray (ds : List Float) : FloatArray

Converts a list of floats into a FloatArray.

def List.toFloatArray.loop : List Float → FloatArray → FloatArray

instance instToStringFloatArray : ToString FloatArray