Lean 4.0.0, first official lean4 release

Re:Lean 4.0.0, first official lean4 release by incrudible on Friday September 08, 2023 @09:52AM (#37433503)

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")[];

[ Parent | on HN ]

Re:Lean 4.0.0, first official lean4 release by ykonstant on Friday September 08, 2023 @10:40AM (#37434103)

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}"

[ Parent | on HN ]