structure FloatArray : Type

• data : Array Float

@[extern lean_mk_empty_float_array]

def FloatArray.mkEmpty (c : Nat) : FloatArray

Equations

• FloatArray.mkEmpty c = { data := #[] }

def FloatArray.empty : FloatArray

Equations

• FloatArray.empty = FloatArray.mkEmpty 0

instance FloatArray.instInhabited : Inhabited FloatArray

Equations

• FloatArray.instInhabited = { default := FloatArray.empty }

instance FloatArray.instEmptyCollection : EmptyCollection FloatArray

Equations

• FloatArray.instEmptyCollection = { emptyCollection := FloatArray.empty }

@[extern lean_float_array_push]

def FloatArray.push : FloatArray → Float → FloatArray

Equations

• x✝.push x = match x✝, x with | { data := ds }, b => { data := ds.push b }

@[extern lean_float_array_size]

def FloatArray.size : FloatArray → Nat

Equations

• x.size = match x with | { data := ds } => ds.size

@[extern lean_float_array_uget]

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

Equations

• x✝¹.uget x✝ x = match x✝¹, x✝, x with | { data := ds }, i, h => ds[i]

@[extern lean_float_array_fget]

def FloatArray.get (ds : FloatArray) : Fin ds.size → Float

Equations

• x✝.get x = match x✝, x with | { data := ds }, i => ds.get i

@[extern lean_float_array_get]

def FloatArray.get! : FloatArray → Nat → Float

Equations

• x✝.get! x = match x✝, x with | { data := ds }, i => ds.get! i

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

Equations

• ds.get? i = if h : i < ds.size then some (ds.get ⟨i, h⟩) else none

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

Equations

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

instance FloatArray.instLawfulGetElemNatFloatLtSize : LawfulGetElem FloatArray Nat Float fun (xs : FloatArray) (i : Nat) => i < xs.size

Equations

• FloatArray.instLawfulGetElemNatFloatLtSize = ⋯

instance FloatArray.instGetElemUSizeFloatLtNatValValSize : GetElem FloatArray USize Float fun (xs : FloatArray) (i : USize) => ↑i.val < xs.size

Equations

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

instance FloatArray.instLawfulGetElemUSizeFloatLtNatValValSize : LawfulGetElem FloatArray USize Float fun (xs : FloatArray) (i : USize) => ↑i.val < xs.size

Equations

• FloatArray.instLawfulGetElemUSizeFloatLtNatValValSize = ⋯

@[extern lean_float_array_uset]

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

Equations

• x✝².uset x✝¹ x✝ x = match x✝², x✝¹, x✝, x with | { data := ds }, i, v, h => { data := ds.uset i v h }

@[extern lean_float_array_fset]

def FloatArray.set (ds : FloatArray) : Fin ds.size → Float → FloatArray

Equations

• x✝¹.set x✝ x = match x✝¹, x✝, x with | { data := ds }, i, d => { data := ds.set i d }

@[extern lean_float_array_set]

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

Equations

• x✝¹.set! x✝ x = match x✝¹, x✝, x with | { data := ds }, i, d => { data := ds.set! i d }

def FloatArray.isEmpty (s : FloatArray) : Bool

Equations

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

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

Equations

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

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.

Equations

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

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

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

• as.forIn b f = FloatArray.forIn.loop as f as.size ⋯ b

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

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

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

Equations

• FloatArray.instForInFloat = { forIn := fun {β : Type u_1} [Monad m] => FloatArray.forIn }

@[inline]

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

See comment at forInUnsafe

Equations

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

@[specialize #[]]

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

Equations

• FloatArray.foldlMUnsafe.fold f as i stop b = if (i == stop) = true then pure b else do let __do_lift ← f b (as.uget i ⋯) FloatArray.foldlMUnsafe.fold f as (i + 1) stop __do_lift

@[implemented_by FloatArray.foldlMUnsafe]

def FloatArray.foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float → m β) (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.

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 : Nat) (j : Nat) (b : β) : m β

Equations

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

@[inline]

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

Equations

• FloatArray.foldl f init as start stop = (FloatArray.foldlM f init as start stop).run

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

Equations

• ds.toFloatArray = List.toFloatArray.loop ds FloatArray.empty

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

Equations

• List.toFloatArray.loop [] x = x
• List.toFloatArray.loop (b :: ds) x = List.toFloatArray.loop ds (x.push b)

instance instToStringFloatArray : ToString FloatArray

Equations

• instToStringFloatArray = { toString := fun (ds : FloatArray) => ds.toList.toString }