@[inline]
unsafe def
FloatArray.mapMUnsafe
{m : Type → Type u_1}
[Monad m]
(a : FloatArray)
(f : Float → m Float)
:
Unsafe optimized implementation of mapM
.
This function is unsafe because it relies on the implementation limit that the size of an array is
always less than USize.size
.
Equations
- a.mapMUnsafe f = FloatArray.mapMUnsafe.loop f a 0 a.usize
Instances For
@[specialize #[]]
unsafe def
FloatArray.mapMUnsafe.loop
{m : Type → Type u_1}
[Monad m]
(f : Float → m Float)
(a : FloatArray)
(k s : USize)
:
Inner loop for mapMUnsafe
.
Equations
- FloatArray.mapMUnsafe.loop f a k s = if k < s then let x := a.uget k ⋯; do let y ← f x let a : FloatArray := a.uset k y ⋯ FloatArray.mapMUnsafe.loop f a (k + 1) s else pure a
Instances For
@[implemented_by FloatArray.mapMUnsafe]
mapM f a
applies the monadic function f
to each element of the array.
Equations
- One or more equations did not get rendered due to their size.