mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 01:09:03 +03:00
a972778eab
They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
23 lines
409 B
Idris
23 lines
409 B
Idris
infixr 5 ::
|
|
|
|
namespace List
|
|
public export
|
|
data List a = Nil | (::) a (List a)
|
|
|
|
namespace Stream
|
|
public export
|
|
data Stream a = (::) a (Inf (Stream a))
|
|
|
|
ones : Stream Integer
|
|
ones = num :: ones
|
|
where
|
|
num : Integer -- gratuitous where for a regression test!
|
|
num = 1
|
|
|
|
data Nat = Z | S Nat
|
|
|
|
take : Nat -> Stream a -> List a
|
|
take Z xs = Nil
|
|
take (S k) (x :: xs) = List.(::) x (take k xs)
|
|
|