2
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$ Dec 3, 2023 at 21:17

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
2
  • 3
    $\begingroup$ Whoever thought that default auto-implicits were a good idea is going to the fifth circle. $\endgroup$ Dec 4, 2023 at 7:20
  • $\begingroup$ 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? $\endgroup$ Feb 29 at 1:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.