Documentation
Init
.
Data
.
Vector
.
Stream
Search
return to top
source
Imports
Init.Data.Stream
Init.Data.Vector.Basic
Imported by
Vector
.
instToStreamSubarray
ToStream instance
#
source
instance
Vector
.
instToStreamSubarray
{
α
:
Type
u_1}
{
n
:
Nat
}
:
Std.ToStream
(
Vector
α
n
)
(
Subarray
α
)
Equations
Vector.instToStreamSubarray
=
{
toStream
:=
fun (
xs
:
Vector
α
n
) =>
Std.Rii.Sliceable.mkSlice
xs
.
toArray
*...*
}