依存型のあるHaskellことIdrisってどんな言語？ | κeenのHappy Hacκing Blog

import Data.String data FizzBuzz = F | B | FB | I Integer Show FizzBuzz where show F = "fizz" show B = "buzz" show FB = "fizzbuzz" show (I n) = show n fizzBuzz : Integer -> FizzBuzz fizzBuzz n = case (n `mod` 3, n `mod` 5) of (0, 0) => FB (_, 0) => B (0, _) => F _ => I n fizzBuzzSeq : Integer -> List FizzBuzz fizzBuzzSeq n = map fizzBuzz [1..n] main : IO () main = do [_, arg] <- getArgs | _ => put