Code generation failed error

Stream: new members

[ROCKY KAMEN-RUBIO]

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]

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]

If you hadn't written noncomputable theory you'd have to put noncomputable before f, and that would be a clue

[ROCKY KAMEN-RUBIO]

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]

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]

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]

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!)