5 ms·
Lean will not create a custom type to infer for each function; it will either infer an existing type or report failure; it will also not automatically coerce to
by ykonstant 3y ago
Lean will not create a custom type to infer for each function; it will either infer an existing type or report failure; it will also not automatically coerce to String. What you see above is a proof in tactic mode of your specification as a theorem. If you want to guarantee the outputs of a function, you need to specify a custom type. For instance:
inductive FizzBuzz where
| fizz
| buzz
| fizzBuzz
| none
def fizzBuzz (n : Nat) : FizzBuzz :=
if n % 15 == 0 then .fizzBuzz
else if n % 3 == 0 then .fizz
else if n % 5 == 0 then .buzz
else .none
instance : ToString FizzBuzz where
toString : FizzBuzz → String
| .none => ""
| .fizz => "Fizz"
| .buzz => "Buzz"
| .fizzBuzz => "FizzBuzz"
def stringFizz (n : Nat) : String :=
toString <| fizzBuzz n
def printFizz (n : Nat) : IO Unit := do
println! s!"{fizzBuzz n}"