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

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.

• I think the issue might be that Rat doesn't actually exist and is being interpreted as the name of a constraint instead of the name of an actual type? In that case what is the type actually called. Dec 3, 2023 at 21:17

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.

• Whoever thought that default auto-implicits were a good idea is going to the fifth circle. Dec 4, 2023 at 7:20
• Related, does " Real (good for proofs, but can’t be used for computation)" mean I cannot construct a real number in lean? like def c : Real := 3? Feb 29 at 1:34