martinsson

%default total

-- Proofs that a value is divisible my 3 and 5 respectively
IsFizz : (k : Nat) -> Type
IsFizz k = (modNatNZ k 3 SIsNotZ = 0)

IsBuzz : Nat -> Type
IsBuzz k = (modNatNZ k 5 SIsNotZ = 0)

-- The type Fizzbuzz, one can only construct an instance of Fizz if one can provide

DASPRiD

Used font: http://stuff.dasprids.de/fonts/ubuntumono-powerline.tar.bz2

You can patch any font yourself with the fontpatcher: https://github.com/Lokaltog/vim-powerline/tree/develop/fontpatcher