mirror of
https://github.com/polarity-lang/polarity.git
synced 2025-12-23 09:19:50 +00:00
13 lines
435 B
Text
13 lines
435 B
Text
/// The codata type of infinite streams.
|
|
codata Stream(a: Type) {
|
|
/// The head observation which yields the first element.
|
|
Stream(a).hd(implicit a: Type): a,
|
|
/// The tail observation which yields the remainder of the stream.
|
|
Stream(a).tl(implicit a: Type): Stream(a),
|
|
}
|
|
|
|
/// An infinite stream which repeats the argument.
|
|
codef Repeat(a: Type, elem: a): Stream(a) {
|
|
.hd(_) => elem,
|
|
.tl(_) => Repeat(a, elem),
|
|
}
|