@[extern lean_mk_empty_float_array]
Equations
- FloatArray.mkEmpty c = { data := #[] }
Equations
- FloatArray.instInhabitedFloatArray = { default := FloatArray.empty }
Equations
- FloatArray.instEmptyCollectionFloatArray = { emptyCollection := FloatArray.empty }
@[extern lean_float_array_push]
Equations
- FloatArray.push x x = match x, x with | { data := ds }, b => { data := Array.push ds b }
@[extern lean_float_array_size]
Equations
- FloatArray.size x = match x with | { data := ds } => Array.size ds
@[extern lean_float_array_uget]
Equations
- FloatArray.uget x x x = match x, x, x with | { data := ds }, i, h => Array.uget ds i h
@[extern lean_float_array_fget]
Equations
- FloatArray.get x x = match x, x with | { data := ds }, i => Array.get ds i
@[extern lean_float_array_get]
Equations
- FloatArray.get! x x = match x, x with | { data := ds }, i => Array.get! ds i
Equations
- FloatArray.get? ds i = if h : i < FloatArray.size ds then some (FloatArray.get ds { val := i, isLt := h }) else none
@[inline]
Equations
- FloatArray.getOp self idx = FloatArray.get! self idx
@[extern lean_float_array_uset]
def
FloatArray.uset
(a : FloatArray)
(i : USize)
:
(a : 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]
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]
Equations
- FloatArray.set! x x x = match x, x, x with | { data := ds }, i, d => { data := Array.set! ds i d }
Equations
- FloatArray.isEmpty s = (FloatArray.size s == 0)
Equations
- FloatArray.toList ds = (fun loop => loop 0 []) (FloatArray.toList.loop ds)
@[inline]
unsafe def
FloatArray.forInUnsafe
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(as : FloatArray)
(b : β)
(f : Float → β → m (ForInStep β))
:
m β
Equations
- FloatArray.forInUnsafe as b f = let sz := USize.ofNat (FloatArray.size as); (fun loop => loop 0 b) (FloatArray.forInUnsafe.loop as f sz)
@[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
- FloatArray.forInUnsafe.loop as f sz i b = if i < sz then let a := FloatArray.uget as i (_ : USize.toNat i < FloatArray.size as); do let a ← f a b match a with | ForInStep.done b => pure b | ForInStep.yield b => FloatArray.forInUnsafe.loop as f sz (i + 1) b else pure b
@[implementedBy FloatArray.forInUnsafe]
noncomputable def
FloatArray.forIn
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(as : FloatArray)
(b : β)
(f : Float → β → m (ForInStep β))
:
m β
Equations
- FloatArray.forIn as b f = (fun loop => loop (FloatArray.size as) (_ : FloatArray.size as ≤ FloatArray.size as) b) (FloatArray.forIn.loop as f)
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
- FloatArray.forIn.loop as f 0 x b = pure b
- FloatArray.forIn.loop as f (Nat.succ i_2) h_2 b = (fun h' => let_fun this := (_ : FloatArray.size as - 1 < FloatArray.size as); let_fun this := (_ : FloatArray.size as - 1 - i_2 < FloatArray.size as); do let a ← f (FloatArray.get as { val := FloatArray.size as - 1 - i_2, isLt := this }) b match a with | ForInStep.done b => pure b | ForInStep.yield b => FloatArray.forIn.loop as f i_2 (_ : i_2 ≤ FloatArray.size as) b) (_ : i_2 < FloatArray.size as)
@[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 β
Equations
- FloatArray.foldlMUnsafe f init as start stop = (fun fold => if start < stop then if stop ≤ FloatArray.size as then fold (USize.ofNat start) (USize.ofNat stop) init else pure init else pure init) (FloatArray.foldlMUnsafe.fold f as)
@[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
- FloatArray.foldlMUnsafe.fold f as i stop b = if (i == stop) = true then pure b else do let a ← f b (FloatArray.uget as i (_ : USize.toNat i < FloatArray.size as)) FloatArray.foldlMUnsafe.fold f as (i + 1) stop a
@[implementedBy FloatArray.foldlMUnsafe]
noncomputable 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 β
Equations
- FloatArray.foldlM f init as start stop = let fold := fun stop h => (fun loop => loop (stop - start) start init) (FloatArray.foldlM.loop f as stop h); if h : stop ≤ FloatArray.size as then fold stop h else fold (FloatArray.size as) (_ : FloatArray.size as ≤ FloatArray.size as)
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
- FloatArray.foldlM.loop f as stop h 0 j b = if hlt : j < stop then pure b else pure b
- FloatArray.foldlM.loop f as stop h (Nat.succ i') j b = if hlt : j < stop then do let a ← f b (FloatArray.get as { val := j, isLt := (_ : j < FloatArray.size as) }) FloatArray.foldlM.loop f as stop h i' (j + 1) a else pure b
@[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)
Equations
- List.toFloatArray ds = (fun loop => loop ds FloatArray.empty) List.toFloatArray.loop
Equations
- List.toFloatArray.loop [] x = x
- List.toFloatArray.loop (b :: ds) x = List.toFloatArray.loop ds (FloatArray.push x b)
Equations
- instToStringFloatArray = { toString := fun ds => List.toString (FloatArray.toList ds) }