## Stream: new members

### Topic: deep recursion

#### Richard Copley (Aug 22 2023 at 15:47):

I get a "(kernel) deep recursion detected" error, in the last def in this code:

import Mathlib.Data.Int.Basic
import Mathlib.Tactic.NormNum

def prop0 (x : ) := x  0
def prop1 (x : ) := x.natAbs / 2 ^ (Nat.size (x.natAbs) - 24) * 2 ^ (Nat.size (x.natAbs) - 24) = x.natAbs

inductive float where
| normal (val : {x :  // prop0 x  prop1 x})

-- Can construct a float from the value (2 ^ 23 : ℤ):

theorem has_prop0 : prop0 (2 ^ 23) := by
unfold prop0
simp

theorem has_prop1 : prop1 (2 ^ 23) := by
unfold prop1
rewrite [(by rfl : (2 ^ 23 : ).natAbs = 2 ^ 23)]
rewrite [Nat.size_pow]
norm_num

def x₀ : float := float.normal 2 ^ 23, has_prop0, has_prop1

-- Cannot construct from same value if the proof of prop1 val is inlined:

def x₁ : float :=
--  ~~ error: "(kernel) deep recursion detected"
let val :  := 2 ^ 23
have h₀ : prop0 val := has_prop0
have h₁ : prop1 val := by
unfold prop1
rewrite [(by rfl : val.natAbs = 2 ^ 23)]
rewrite [Nat.size_pow]
norm_num
float.normal val, h₀, h₁

Why does this happen? Is there a well-known way to avoid it? If not, can you give me any hints on how to get more details about the recursion from Lean, for debugging?

#### Kevin Buzzard (Aug 22 2023 at 15:59):

Using rfl and large numbers is dangerous. Changing it to this

rewrite [(by norm_num : val.natAbs = 2 ^ 23)]

works.

#### Richard Copley (Aug 22 2023 at 16:06):

Perfect, thanks.

Last updated: Dec 20 2023 at 11:08 UTC