Idris2/tests/idris2/misc/lazy001/Lazy.idr

private 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)
Emit warning for fixities with no export modifiers (#3234) * Emit warning for fixities with no export modifiers This is to help update all the existing code to program with explicit fixity export directives in preparation for the behavioral change where they will become private by default. 2024-04-03 17:41:57 +03:00			`private infixr 5 ::`
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00
			`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)`