module Test.Division-Foreign where

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

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)))