Recursively Defined Sequence Across Types

Stream: new members

[Logan Johnson]

Hello, I am now trying to define a recursive sequence from the naturals onto the reals, but am running into issues with the function actually evaluating. I am trying to get a function such that the first term is 1, and the (n + 1)th term is (2 + nth term)^(1/2). I have tried to define this function like this:

def myFunc : ℕ → ℝ
  | 0 => 1
  | n + 1 =>  (2 + myFunc n)^(1/2)

However, this gives the following error:

fail to show termination for
  myFunc
with errors
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instLinearOrderedFieldReal', and it does not have executable code

I have no idea how else I could define this function. I also seemed to be having some issues simply taking the square root of a real number, is there anything that could be done about that?

Thanks.

[Eric Wieser]

That error is telling you that you need to put noncomputable at the start of the first line