2
$\begingroup$

How do I fix

limit_linear_khan_academy.lean:22:16
Messages (1)
limit_linear_khan_academy.lean:22:13
failed to synthesize instance
  OfScientific ℝ
All Messages (4)

code?

def c : ℝ := 0.5
$\endgroup$
2
  • 3
    $\begingroup$ You should provide a self-contained piece of code, so that anyone can directly pull up the code and see the error for themselves. $\endgroup$
    – Trebor
    Commented Mar 17 at 3:46
  • 1
    $\begingroup$ My guess is that you didn’t import the reals. Try import Mathlib at the top. Without that or similar, Lean thinks ℝ is a new type. This “feature” is quite controversial. (Also the Reals are not in base Lean.) $\endgroup$
    – Jason Rute
    Commented Mar 30 at 2:04

1 Answer 1

4
$\begingroup$

You need to import Real numbers:

import Mathlib.Data.Real.Basic

def c : ℝ := 0.5
#eval c

output

Real.ofCauchy (sorry /- (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, ... -/)
```
$\endgroup$

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.