Equations
- FloatArray.instInhabited = { default := FloatArray.empty }
Equations
- FloatArray.instEmptyCollection = { emptyCollection := FloatArray.empty }
@[extern lean_float_array_push]
Equations
- x✝.push x = match x✝, x with | { data := ds }, b => { data := ds.push b }
Instances For
@[extern lean_float_array_size]
Equations
- x.size = match x with | { data := ds } => ds.size
Instances For
@[extern lean_float_array_uget]
Equations
- x✝¹.uget x✝ x = match x✝¹, x✝, x with | { data := ds }, i, h => ds[i]
Instances For
@[extern lean_float_array_fget]
Equations
- x✝.get x = match x✝, x with | { data := ds }, i => ds.get i
Instances For
@[extern lean_float_array_get]
Equations
- x✝.get! x = match x✝, x with | { data := ds }, i => ds.get! i
Instances For
Instances For
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
FloatArray.instGetElemUSizeFloatLtNatValValSize :
GetElem FloatArray USize Float fun (xs : FloatArray) (i : USize) => ↑i.val < xs.size
Equations
- FloatArray.instGetElemUSizeFloatLtNatValValSize = { getElem := fun (xs : FloatArray) (i : USize) (h : ↑i.val < xs.size) => xs.uget i h }
@[extern lean_float_array_uset]
Equations
- x✝².uset x✝¹ x✝ x = match x✝², x✝¹, x✝, x with | { data := ds }, i, v, h => { data := ds.uset i v h }
Instances For
@[extern lean_float_array_fset]
Equations
- x✝¹.set x✝ x = match x✝¹, x✝, x with | { data := ds }, i, d => { data := ds.set i d }
Instances For
@[extern lean_float_array_set]
Equations
- x✝¹.set! x✝ x = match x✝¹, x✝, x with | { data := ds }, i, d => { data := ds.set! i d }
Instances For
Equations
- ds.toList = FloatArray.toList.loop ds 0 []
Instances For
@[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
Instances For
@[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
Instances For
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
Instances For
@[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.
Instances For
@[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
Instances For
@[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.
Instances For
@[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
Instances For
Equations
- ds.toFloatArray = List.toFloatArray.loop ds FloatArray.empty
Instances For
Equations
- List.toFloatArray.loop [] x = x
- List.toFloatArray.loop (b :: ds) x = List.toFloatArray.loop ds (x.push b)
Instances For
Equations
- instToStringFloatArray = { toString := fun (ds : FloatArray) => ds.toList.toString }