FizzBuzz.idr

import Data.So

fizz : Integer -> Bool
fizz n = (n `mod` 3) == 0

buzz : Integer -> Bool
buzz n = (n `mod` 5) == 0

data FizzBuzz : (n: Integer) -> Type where
  Fizz : {auto fizz : So (fizz n)} -> FizzBuzz n
  Buzz : {auto buzz : So (buzz n)} -> FizzBuzz n

Show (FizzBuzz n) where 
  show Fizz = "Fizz"
  show Buzz = "Buzz"

fizzBuzz : (n: Integer) -> List (FizzBuzz n)
fizzBuzz n  = case (choose (fizz n),choose (buzz n)) of
             (Left _,Right _) => [Fizz]
             (Right _,Left _) => [Buzz]
             (Left _,Left _) => [Fizz,Buzz]
             (Right _,Right _) => []

showFizzBuzz : Integer -> String
showFizzBuzz n = case (fizzBuzz n) of
                      [] => show n
                      f => concatMap show f