4 ms·
Thank you. I must admit, I have trouble making sense of it. Just for comparison, in Typescript you can write: function f(n:number){ if (n%3==0 && n%5==0
by incrudible 3y ago
Thank you. I must admit, I have trouble making sense of it.
Just for comparison, in Typescript you can write:
function f(n:number){
if (n%3==0 && n%5==0) return "FizzBuzz"
if (n%3==0) return "Fizz"
if (n%5==0) return "Buzz"
return "";
}
The return type of this function will be inferred as "Fizz"|"Buzz"|"FizzBuzz"|"".
Then, I can write:
function *iFizzBuzz(steps:number){
for (let i=0; i<steps; i++){
const fb = f(i);
if (fb) yield fb;
}
}
const fizzBuzz100 = Array.from(iFizzBuzz(100));
The type of fizzBuzz100 will be inferred as ("Fizz"|"Buzz"|"FizzBuzz")[];
- ykonstant 3y agoLean 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}"