Documentation

Init.Data.FloatArray.Basic

structure FloatArray :

data : Array Float

Instances For

@[extern lean_mk_empty_float_array]

def FloatArray.mkEmpty (c : Nat) :

Equations

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

def FloatArray.empty :

Equations

FloatArray.empty = FloatArray.mkEmpty 0

instance FloatArray.instInhabitedFloatArray :

Inhabited FloatArray

Equations

FloatArray.instInhabitedFloatArray = { default := FloatArray.empty }

instance FloatArray.instEmptyCollectionFloatArray :

EmptyCollection FloatArray

Equations

FloatArray.instEmptyCollectionFloatArray = { emptyCollection := FloatArray.empty }

@[extern lean_float_array_push]

def FloatArray.push :

FloatArray → Float → FloatArray

Equations

FloatArray.push x x = match x, x with | { data := ds }, b => { data := Array.push ds b }

@[extern lean_float_array_size]

def FloatArray.size :

FloatArray → Nat

Equations

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

@[extern lean_float_array_uget]

def FloatArray.uget (a : FloatArray) (i : USize) :

USize.toNat i < FloatArray.size a → Float

Equations

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

@[extern lean_float_array_fget]

def FloatArray.get (ds : FloatArray) :

Fin (FloatArray.size ds) → Float

Equations

FloatArray.get x x = match x, x with | { data := ds }, i => Array.get ds i

@[extern lean_float_array_get]

def FloatArray.get! :

FloatArray → Nat → Float

Equations

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

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

Equations

FloatArray.get? ds i = if h : i < FloatArray.size ds then some (FloatArray.get ds { val := i, isLt := h }) else none

instance FloatArray.instGetElemFloatArrayNatFloatLtInstLTNatSize :

GetElem FloatArray Nat Float fun xs i => i < FloatArray.size xs

Equations

FloatArray.instGetElemFloatArrayNatFloatLtInstLTNatSize = { getElem := fun xs i h => FloatArray.get xs { val := i, isLt := h } }

instance FloatArray.instGetElemFloatArrayUSizeFloatLtNatInstLTNatValSizeValSize :

GetElem FloatArray USize Float fun xs i => i.val.val < FloatArray.size xs

Equations

FloatArray.instGetElemFloatArrayUSizeFloatLtNatInstLTNatValSizeValSize = { getElem := fun xs i h => FloatArray.uget xs i h }

@[extern lean_float_array_uset]

def FloatArray.uset (a : FloatArray) (i : USize) :

Float → USize.toNat i < FloatArray.size a → FloatArray

Equations

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

@[extern lean_float_array_fset]

def FloatArray.set (ds : FloatArray) :

Fin (FloatArray.size ds) → Float → FloatArray

Equations

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

@[extern lean_float_array_set]

def FloatArray.set! :

FloatArray → Nat → Float → FloatArray

Equations

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

def FloatArray.isEmpty (s : FloatArray) :

Equations

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

def FloatArray.toList (ds : FloatArray) :

Equations

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

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

@[inline]

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

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

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

@[implemented_by FloatArray.forInUnsafe]

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

m β

Reference implementation for forIn

Equations

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

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

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

ForIn m FloatArray Float

Equations

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

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

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

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

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} [inst : Monad m] (f : β → Float → m β) (as : FloatArray) (stop : Nat) (h : stop ≤ FloatArray.size as) (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 (FloatArray.size as)) :

β

Equations

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

def List.toFloatArray (ds : List Float) :

Equations

List.toFloatArray ds = 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 (FloatArray.push x b)

instance instToStringFloatArray :

ToString FloatArray

Equations

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