structure FloatArray : Type

• data : Array Float

def FloatArray.instBEq.beq : FloatArray → FloatArray → Bool

Equations

• FloatArray.instBEq.beq { data := a } { data := b } = (a == b)
• FloatArray.instBEq.beq x✝¹ x✝ = false

@[instance_reducible]

instance FloatArray.instBEq : BEq FloatArray

Equations

• FloatArray.instBEq = { beq := FloatArray.instBEq.beq }

theorem FloatArray.ext {x y : FloatArray} (data : x.data = y.data) : x = y

theorem FloatArray.ext_iff {x y : FloatArray} : x = y ↔ x.data = y.data

@[extern lean_mk_empty_float_array]

def FloatArray.emptyWithCapacity (c : Nat) : FloatArray

Equations

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

def FloatArray.empty : FloatArray

Equations

• FloatArray.empty = FloatArray.emptyWithCapacity 0

@[instance_reducible]

instance FloatArray.instInhabited : Inhabited FloatArray

Equations

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

@[instance_reducible]

instance FloatArray.instEmptyCollection : EmptyCollection FloatArray

Equations

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

@[extern lean_float_array_push]

def FloatArray.push : FloatArray → Float → FloatArray

Equations

• { data := ds }.push x✝ = { data := ds.push x✝ }

@[extern lean_float_array_size]

def FloatArray.size : FloatArray → Nat

Equations

• { data := ds }.size = ds.size

@[extern lean_sarray_size]

def FloatArray.usize (a : FloatArray) : USize

Equations

• a.usize = a.size.toUSize

@[extern lean_float_array_uget]

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

Equations

• { data := ds }.uget x✝¹ x✝ = ds[x✝¹]

@[extern lean_float_array_fget]

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

Equations

• { data := ds }.get x✝¹ x✝ = ds[x✝¹]

@[extern lean_float_array_get]

def FloatArray.get! : FloatArray → Nat → Float

Equations

• { data := ds }.get! x✝ = ds[x✝]!

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_reducible]

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

Equations

• FloatArray.instGetElemNatFloatLtSize = { getElem := fun (xs : FloatArray) (i : Nat) (h : i < xs.size) => xs.get i h }

@[instance_reducible]

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

Equations

• FloatArray.instGetElemUSizeFloatLtNatToNatSize = { getElem := fun (xs : FloatArray) (i : USize) (h : i.toNat < xs.size) => xs.uget i h }

@[extern lean_float_array_uset]

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

Equations

• { data := ds }.uset x✝² x✝¹ x✝ = { data := ds.uset x✝² x✝¹ x✝ }

@[extern lean_float_array_fset]

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

Equations

• { data := ds }.set x✝² x✝¹ x✝ = { data := ds.set x✝² x✝¹ x✝ }

@[extern lean_float_array_set]

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

Equations

• { data := ds }.set! x✝¹ x✝ = { data := ds.set! x✝¹ x✝ }

@[never_extract, extern lean_sarray_mark_linear]

def FloatArray.markLinear (ds : FloatArray) : FloatArray

Marks a float array as linear, which is a no-op logically.

At runtime the array is first made unique, copying it if the reference is not already unique, and then marked. If the environment variable LEAN_ABORT_ON_NONLINEAR is set, every non-linear use from that point on causes a panic instead of a silent copy.

To debug where the non-linearity is coming from you can set a breakpoint on lean_internal_panic.

Equations

• ds.markLinear = ds

@[simp]

theorem FloatArray.markLinear_eq {ds : FloatArray} : ds.markLinear = ds

@[never_extract, extern lean_sarray_propagate_mark]

def FloatArray.propagateMark (ds : FloatArray) (es : FloatArray) : FloatArray

Returns es, propagating the linearity marker of ds onto it. This is a no-op logically.

See also FloatArray.markLinear.

Equations

• ds.propagateMark es = es

@[simp]

theorem FloatArray.propagateMark_eq {ds es : FloatArray} : ds.propagateMark es = es

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

@[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 = FloatArray.forInUnsafe.loop✝ as f as.usize 0 b

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

@[instance_reducible]

instance FloatArray.instForInFloatOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m FloatArray Float

Equations

• FloatArray.instForInFloatOfMonad = { forIn := fun {β : Type ?u.2} => FloatArray.forIn }

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

Equations

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

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

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 : Nat := 0) (stop : Nat := as.size) : β

Equations

• FloatArray.foldl f init as start stop = (FloatArray.foldlM (fun (x1 : β) (x2 : Float) => pure (f x1 x2)) init as start stop).run

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

Converts a list of floats into a FloatArray.

Equations

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

@[instance_reducible]

instance instToStringFloatArray : ToString FloatArray

Equations

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