RosettaCodeData/Task/FizzBuzz/Lean/fizzbuzz.lean

39 lines
781 B
Plaintext

def fizz : String :=
"Fizz"
def buzz : String :=
"Buzz"
def newLine : String :=
"\n"
def isDivisibleBy (n : Nat) (m : Nat) : Bool :=
match m with
| 0 => false
| (k + 1) => (n % (k + 1)) = 0
def getTerm (n : Nat) : String :=
if (isDivisibleBy n 15) then (fizz ++ buzz)
else if (isDivisibleBy n 3) then fizz
else if (isDivisibleBy n 5) then buzz
else toString (n)
def range (a : Nat) (b : Nat) : List (Nat) :=
match b with
| 0 => []
| m + 1 => a :: (range (a + 1) m)
def getTerms (n : Nat) : List (String) :=
(range 1 n).map (getTerm)
def addNewLine (accum : String) (elem : String) : String :=
accum ++ elem ++ newLine
def fizzBuzz : String :=
(getTerms 100).foldl (addNewLine) ("")
def main : IO Unit :=
IO.println (fizzBuzz)
#eval main