Comment by kristopolous

I really find how theoreticians approach things to be challenging. Given that I headed to rosetta code to find some examples. Here's FizzBuzz in Lean 4:

https://rosettacode.org/wiki/FizzBuzz#Lean

  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

Hopefully that's helpful to others.