How do I make the rational numbers 0 and 1/2 in lean4?

Question

I'm trying to define a function that in python I would write:

def f(x: bool) -> float:
    if x:
        return 0.5
    return 0.0

In lean 4 I tried writing this (this is the whole file):

def f (b : Bool) : Rat :=
match b with
| false => 0
| true => 0.5

But I get type errors:

failed to synthesize instance
  OfNat Rat 0
failed to synthesize instance
  OfScientific Rat

It seems to be having trouble turning the number literals I wrote into the type Rat that I want. Probably I just need to invoke some conversion method on the literals to do the cast, but I don't know what that method is called and it's unfortunately basically impossible to google for the names of methods this basic.

Answer 1

You unfortunately ran into the dark side of auto-implict arguments. Since Rat wasn’t in scope, Lean automatically added it as an implicit parameter.

Rat can be found in Std.Data.Rat (you need to make sure the standard library is included in your project).

import Std.Data.Rat

def f (b : Bool) : Rat := if b then 0.5 else 0

#eval f true  -- (1 : Rat)/2
#eval f false -- 0

A good way to look this stuff up is in the mathlib documentation, which is more than just mathlib. Lean also has other number types like Float (good for computation, but annoying for proofs) and Real (good for proofs, but can’t be used for computation). Rat is indeed a good middle ground between the two.