Test.Division-Native

module Test.Division-Native where

open import Data.ForeignNat
open import Data.ForeignNat.Show

open import Data.Bool using (Bool; true; false)
open import Relation.Nullary
open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Char  
open import Data.List

open import IO
import Data.Colist

even : ℕ → Bool
even n  with 2 ∣? n
...     | yes  _  = true
...     | no   _  = false

numbersBelow : ℕ → List ℕ
numbersBelow zero     = []
numbersBelow (suc n)  = numbersBelow n ++ [ n ]

evenNumbers = filter even numbers
   where numbers = numbersBelow 1000

main = run (mapM′ putStrLn∞ (Data.Colist.fromList (Data.List.map show evenNumbers)))