Zulip Chat Archive

Stream: new members

Topic: Recursively Defined Sequence Across Types

Logan Johnson (Oct 10 2023 at 22:03):

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
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?


Eric Wieser (Oct 10 2023 at 22:05):

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

Last updated: Dec 20 2023 at 11:08 UTC