# Zulip Chat Archive

## Stream: new members

### Topic: Code generation failed error

#### ROCKY KAMEN-RUBIO (May 28 2020 at 17:53):

I'm trying to work with sequences that use the quadratic formula recursively. When I try to have a simple function like below, I get a `code generation failed, VM does not have code for 'classical.indefinite_description'`

error and haven't been able to find anything on why this is happening.

```
import data.real.basic
import tactic
noncomputable theory
def f : ℝ := (- pn - real.sqrt (pn^2 - 4*qn))/2
#eval f 2 1
```

#### Chris Hughes (May 28 2020 at 17:55):

Reals in Lean are the actual mathematical definition of the reals, they're not floats or any computable definition. This means you can only prove theorems about them, but not compute with them.

#### Reid Barton (May 28 2020 at 17:56):

If you hadn't written `noncomputable theory`

you'd have to put `noncomputable`

before `f`

, and that would be a clue

#### ROCKY KAMEN-RUBIO (May 28 2020 at 18:18):

Removing the `noncomputable theory`

I get `f' is noncomputable, it depends on 'real.division_ring'`

. Does that mean this just isn't something lean can do?

More context: I'd like to show that a sequence formed by recursively applying functions similar to this eventually produces a complex result. Is that just not something mathlib can support yet?

#### Bryan Gin-ge Chen (May 28 2020 at 18:24):

You could definitely formalize such a theorem about that sequence in Lean. You just can't use `#eval`

on any functions that use `real`

s.

#### Alex J. Best (May 28 2020 at 18:34):

Eval is a very specific thing, if you just want lean to simplify and tell you the answer in a proved manner one can do:

```
example : f 2 1 = 1 :=
begin
rw f,
conv_lhs{
norm_num,},
end
```

of course 1 is not the answer, but after norm_num lean has simplified the expression.

#### Jalex Stark (May 29 2020 at 02:52):

to try to cut to the core of the confusion:

how do you expect Lean to do what you've asked? like what algorithm do you expect it to run?

(also I'm guessing you meant to write `def f (pn qn : ℝ) : ℝ := (- pn - real.sqrt (pn^2 - 4*qn))/2`

in your first message? test your code when you post a question!)

Last updated: May 13 2021 at 19:20 UTC